1.1 --- a/src/HOL/Tools/meson.ML	Sun Mar 01 16:48:06 2009 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Sun Mar 01 23:36:12 2009 +0100
     1.3 @@ -92,7 +92,7 @@
     1.4      | pairs =>
     1.5          let val thy = theory_of_thm th
     1.6              val (tyenv,tenv) =
     1.7 -                  foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
     1.8 +                  List.foldl (uncurry (Pattern.first_order_match thy)) (tyenv0,tenv0) pairs
     1.9              val t_pairs = map term_pair_of (Vartab.dest tenv)
    1.10              val th' = Thm.instantiate ([], map (pairself (cterm_of thy)) t_pairs) th
    1.11          in  th'  end
    1.12 @@ -428,7 +428,7 @@
    1.13  fun name_thms label =
    1.14      let fun name1 (th, (k,ths)) =
    1.15            (k-1, Thm.put_name_hint (label ^ string_of_int k) th :: ths)
    1.16 -    in  fn ths => #2 (foldr name1 (length ths, []) ths)  end;
    1.17 +    in  fn ths => #2 (List.foldr name1 (length ths, []) ths)  end;
    1.18  
    1.19  (*Is the given disjunction an all-negative support clause?*)
    1.20  fun is_negative th = forall (not o #1) (literals (prop_of th));
    1.21 @@ -477,7 +477,7 @@
    1.22  (*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
    1.23  fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
    1.24  
    1.25 -fun size_of_subgoals st = foldr addconcl 0 (prems_of st);
    1.26 +fun size_of_subgoals st = List.foldr addconcl 0 (prems_of st);
    1.27  
    1.28  
    1.29  (*Negation Normal Form*)
    1.30 @@ -544,12 +544,12 @@
    1.31  
    1.32  (*Make clauses from a list of theorems, previously Skolemized and put into nnf.
    1.33    The resulting clauses are HOL disjunctions.*)
    1.34 -fun make_clauses ths = sort_clauses (foldr add_clauses [] ths);
    1.35 +fun make_clauses ths = sort_clauses (List.foldr add_clauses [] ths);
    1.36  
    1.37  (*Convert a list of clauses (disjunctions) to Horn clauses (contrapositives)*)
    1.38  fun make_horns ths =
    1.39      name_thms "Horn#"
    1.40 -      (distinct Thm.eq_thm_prop (foldr (add_contras clause_rules) [] ths));
    1.41 +      (distinct Thm.eq_thm_prop (List.foldr (add_contras clause_rules) [] ths));
    1.42  
    1.43  (*Could simply use nprems_of, which would count remaining subgoals -- no
    1.44    discrimination as to their size!  With BEST_FIRST, fails for problem 41.*)