--- a/src/HOL/ex/reflection.ML Wed Oct 04 11:50:37 2006 +0200
+++ b/src/HOL/ex/reflection.ML Wed Oct 04 14:14:33 2006 +0200
@@ -233,9 +233,9 @@
fun mk_congs ctxt raw_eqs =
let
val fs = foldr (fn (eq,fns) =>
- (eq |> prop_of |> HOLogic.dest_Trueprop
+ insert (op =) (eq |> prop_of |> HOLogic.dest_Trueprop
|> HOLogic.dest_eq |> fst |> strip_comb
- |> fst) ins fns) [] raw_eqs
+ |> fst) fns) [] raw_eqs
val tys = foldr (fn (f,ts) => (f |> fastype_of |> binder_types |> split_last |> fst)
union ts) [] fs
val _ = bds := AList.make (fn _ => ([],[])) tys
--- a/src/HOL/ex/svc_funcs.ML Wed Oct 04 11:50:37 2006 +0200
+++ b/src/HOL/ex/svc_funcs.ML Wed Oct 04 14:14:33 2006 +0200
@@ -135,7 +135,7 @@
val nat_vars = ref ([] : string list)
(*translation of a variable: record all natural numbers*)
fun trans_var (a,T,is) =
- (if T = HOLogic.natT then nat_vars := (a ins_string (!nat_vars))
+ (if T = HOLogic.natT then nat_vars := (insert (op =) a (!nat_vars))
else ();
UnInterp (a ^ param_string is, []))
(*A variable, perhaps applied to a series of parameters*)
--- a/src/Pure/proofterm.ML Wed Oct 04 11:50:37 2006 +0200
+++ b/src/Pure/proofterm.ML Wed Oct 04 14:14:33 2006 +0200
@@ -889,7 +889,8 @@
end;
fun needed_vars prop =
- Library.foldl op union ([], map op ins (add_npvars true true [] ([], prop))) union
+ Library.foldl (op union)
+ ([], map (uncurry (insert (op =))) (add_npvars true true [] ([], prop))) union
prop_vars prop;
fun gen_axm_proof c name prop =
--- a/src/Pure/pure_thy.ML Wed Oct 04 11:50:37 2006 +0200
+++ b/src/Pure/pure_thy.ML Wed Oct 04 14:14:33 2006 +0200
@@ -438,7 +438,7 @@
let
val {thy, tpairs, prop, ...} = Thm.rep_thm th;
val add_used = Term.fold_aterms
- (fn Var ((x, j), _) => if i = j then curry (op ins_string) x else I | _ => I);
+ (fn Var ((x, j), _) => if i = j then insert (op =) x else I | _ => I);
val used = fold (fn (t, u) => add_used t o add_used u) tpairs (add_used prop []);
val vars = strip_vars prop;
val cvars = (Name.variant_list used (map #1 vars), vars)