# HG changeset patch
# User haftmann
# Date 1159964073 -7200
# Node ID 3ff5a2e058104680c93cfa4ee7bdea8988e46746
# Parent  edc3147ab164f8a1e92be51a4aa2ee3335dc4440
*** empty log message ***

diff -r edc3147ab164 -r 3ff5a2e05810 src/HOL/ex/reflection.ML
--- 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
diff -r edc3147ab164 -r 3ff5a2e05810 src/HOL/ex/svc_funcs.ML
--- 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*)
diff -r edc3147ab164 -r 3ff5a2e05810 src/Pure/proofterm.ML
--- 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 =
diff -r edc3147ab164 -r 3ff5a2e05810 src/Pure/pure_thy.ML
--- 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)