src/HOL/Tools/meson.ML

--- a/src/HOL/Tools/meson.ML	Thu Oct 29 23:49:55 2009 +0100
+++ b/src/HOL/Tools/meson.ML	Thu Oct 29 23:56:33 2009 +0100
@@ -432,7 +432,7 @@
 
 (*Generate Horn clauses for all contrapositives of a clause. The input, th,
   is a HOL disjunction.*)
-fun add_contras crules (th,hcs) =
+fun add_contras crules th hcs =
   let fun rots (0,th) = hcs
         | rots (k,th) = zero_var_indexes (make_horn crules th) ::
                         rots(k-1, assoc_right (th RS disj_comm))
@@ -443,9 +443,9 @@
 
 (*Use "theorem naming" to label the clauses*)
 fun name_thms label =
-    let fun name1 (th, (k,ths)) =
+    let fun name1 th (k, ths) =
           (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
-    in  fn ths => #2 (List.foldr name1 (length ths, []) ths)  end;
+    in  fn ths => #2 (fold_rev name1 ths (length ths, []))  end;
 
 (*Is the given disjunction an all-negative support clause?*)
 fun is_negative th = forall (not o #1) (literals (prop_of th));
@@ -491,9 +491,9 @@
     TRYALL_eq_assume_tac;
 
 (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
-fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
+fun addconcl prem sz = size_of_term (Logic.strip_assums_concl prem) + sz;
 
-fun size_of_subgoals st = List.foldr addconcl 0 (prems_of st);
+fun size_of_subgoals st = fold_rev addconcl (prems_of st) 0;
 
 
 (*Negation Normal Form*)
@@ -553,19 +553,19 @@
        (trace_msg (fn () => "Failed to Skolemize " ^ Display.string_of_thm ctxt th);
         skolemize_nnf_list ctxt ths);
 
-fun add_clauses (th,cls) =
+fun add_clauses th cls =
   let val ctxt0 = Variable.thm_context th
-      val (cnfs,ctxt) = make_cnf [] th ctxt0
+      val (cnfs, ctxt) = make_cnf [] th ctxt0
   in Variable.export ctxt ctxt0 cnfs @ cls end;
 
 (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
   The resulting clauses are HOL disjunctions.*)
-fun make_clauses ths = sort_clauses (List.foldr add_clauses [] ths);
+fun make_clauses ths = sort_clauses (fold_rev add_clauses ths []);
 
 (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
 fun make_horns ths =
     name_thms "Horn#"
-      (distinct Thm.eq_thm_prop (List.foldr (add_contras clause_rules) [] ths));
+      (distinct Thm.eq_thm_prop (fold_rev (add_contras clause_rules) ths []));
 
 (*Could simply use nprems_of, which would count remaining subgoals -- no
   discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)