--- a/src/Pure/Isar/locale.ML Fri Jul 15 15:44:11 2005 +0200
+++ b/src/Pure/Isar/locale.ML Fri Jul 15 15:44:15 2005 +0200
@@ -623,7 +623,7 @@
let
val {thy, hyps, prop, maxidx, ...} = Thm.rep_thm th;
val cert = Thm.cterm_of thy;
- val (xs, Ts) = Library.split_list (Library.foldl Term.add_frees ([], prop :: hyps));
+ val (xs, Ts) = Library.split_list (fold Term.add_frees (prop :: hyps) []);
val xs' = map (rename ren) xs;
fun cert_frees names = map (cert o Free) (names ~~ Ts);
fun cert_vars names = map (cert o Var o apfst (rpair (maxidx + 1))) (names ~~ Ts);
@@ -705,7 +705,7 @@
fun frozen_tvars ctxt Ts =
let
- val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts));
+ val tvars = rev (fold Term.add_tvarsT Ts []);
val tfrees = map TFree
(Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars);
in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end;
@@ -951,7 +951,7 @@
elemss;
fun inst_ax th = let
val {hyps, prop, ...} = Thm.rep_thm th;
- val ps = map (apsnd SOME) (Library.foldl Term.add_frees ([], prop :: hyps));
+ val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
val [env] = unify_parms ctxt all_params [ps];
val th' = inst_thm ctxt env th;
in th' end;
@@ -1208,7 +1208,7 @@
err "Attempt to define previously specified variable");
conditional (exists (fn (Free (y', _), _) => y = y' | _ => false) env) (fn () =>
err "Attempt to redefine variable");
- (Term.add_frees (xs, b'), (Free (y, T), b') :: env, th :: ths)
+ (Term.add_frees b' xs, (Free (y, T), b') :: env, th :: ths)
end;
(* CB: for finish_elems (Int and Ext) *)
@@ -1222,7 +1222,7 @@
val spec' =
if is_ext then ((exts @ ts, exts' @ ts'), (ints, ints'))
else ((exts, exts'), (ints @ ts, ints' @ ts'));
- in (spec', (Library.foldl Term.add_frees (xs, ts'), env, defs)) end
+ in (spec', (fold Term.add_frees ts' xs, env, defs)) end
| eval_text ctxt (id, _) _ ((spec, binds), Defines defs) =
(spec, Library.foldl (bind_def ctxt id) (binds, map (#1 o #2) defs))
| eval_text _ _ _ (text, Notes _) = text;
@@ -1234,7 +1234,7 @@
let
fun close_frees t =
let val frees = rev (filter_out (ProofContext.is_fixed ctxt o #1)
- (Term.add_frees ([], t)))
+ (Term.add_frees t []))
in Term.list_all_free (frees, t) end;
fun no_binds [] = []
@@ -1966,7 +1966,7 @@
fun sorts (a, i) = assoc (tvars, (a, i));
val (vs, vinst) = read_terms thy_ctxt sorts used given_insts;
val vars = foldl Term.add_term_tvar_ixns [] vs \\ map fst tvars;
- val vars' = Library.foldl Term.add_term_varnames (vars, vs);
+ val vars' = fold Term.add_term_varnames vs vars;
val _ = if null vars' then ()
else error ("Illegal schematic variable(s) in instantiation: " ^
commas_quote (map Syntax.string_of_vname vars'));