--- a/src/HOL/Tools/meson.ML Thu Mar 03 09:22:35 2005 +0100
+++ b/src/HOL/Tools/meson.ML Thu Mar 03 12:43:01 2005 +0100
@@ -164,7 +164,7 @@
fun fewerlits(th1,th2) = nliterals(prop_of th1) < nliterals(prop_of th2);
(*TAUTOLOGY CHECK SHOULD NOT BE NECESSARY!*)
- fun sort_clauses ths = sort (make_ord fewerlits) (filter (not o is_taut) ths);
+ fun sort_clauses ths = sort (make_ord fewerlits) (List.filter (not o is_taut) ths);
(*Convert all suitable free variables to schematic variables*)
fun generalize th = forall_elim_vars 0 (forall_intr_frees th);
@@ -188,12 +188,12 @@
let fun name1 (th, (k,ths)) =
(k-1, Thm.name_thm (label ^ string_of_int k, th) :: ths)
- in fn ths => #2 (foldr name1 (ths, (length ths, []))) end;
+ in fn ths => #2 (Library.foldr name1 (ths, (length ths, []))) end;
(*Find an all-negative support clause*)
fun is_negative th = forall (not o #1) (literals (prop_of th));
- val neg_clauses = filter is_negative;
+ val neg_clauses = List.filter is_negative;
(***** MESON PROOF PROCEDURE *****)
@@ -211,7 +211,7 @@
fun has_reps [] = false
| has_reps [_] = false
| has_reps [t,u] = (t aconv u)
- | has_reps ts = (foldl ins_term (Net.empty, ts); false)
+ | has_reps ts = (Library.foldl ins_term (Net.empty, ts); false)
handle INSERT => true;
(*Like TRYALL eq_assume_tac, but avoids expensive THEN calls*)
@@ -239,7 +239,7 @@
(*Sums the sizes of the subgoals, ignoring hypotheses (ancestors)*)
local fun addconcl(prem,sz) = size_of_term(Logic.strip_assums_concl prem) + sz
in
-fun size_of_subgoals st = foldr addconcl (prems_of st, 0)
+fun size_of_subgoals st = Library.foldr addconcl (prems_of st, 0)
end;
(*Negation Normal Form*)
@@ -265,12 +265,12 @@
(*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 (map (generalize o nodups) (foldr cnf (ths,[])));
+ sort_clauses (map (generalize o nodups) (Library.foldr cnf (ths,[])));
(*Convert a list of clauses to (contrapositive) Horn clauses*)
fun make_horns ths =
name_thms "Horn#"
- (gen_distinct Drule.eq_thm_prop (foldr (add_contras clause_rules) (ths,[])));
+ (gen_distinct Drule.eq_thm_prop (Library.foldr (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.*)