Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.

Add wrapper function for :thm -> thm list.
Promote more objects.

1 files changed, 9 insertions, 0 deletions

diff --git a/hol-light/TacticRecording/lib.ml b/hol-light/TacticRecording/lib.ml
index b1309f84..5de28331 100644
--- a/hol-light/TacticRecording/lib.ml
+++ b/hol-light/TacticRecording/lib.ml
@@ -19,6 +19,15 @@ let rec foldr f xs a =
   | []      -> a;;
 
 
+(* foldr1 : ('a -> 'a -> 'a) -> 'a list -> 'a                                 *)
+
+let rec foldr1 f xs =
+  match xs with
+    x::[]   -> x
+  | x1::xs2 -> f x1 (foldr1 f xs2)
+  | []      -> failwith "foldr1: Empty list";;
+
+
 (* foldl : ('b -> 'a -> 'b) -> 'b -> 'a list -> 'b                            *)
 
 let rec foldl f a xs =