# HG changeset patch
# User wenzelm
# Date 1118046113 -7200
# Node ID 97c9f2c1de3dc08c28ddc4ae1f451ecc65187f56
# Parent  a920fe734a49a93c98206581cb8f5902482d5523
avoid polymorphic ins;

diff -r a920fe734a49 -r 97c9f2c1de3d src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Jun 06 09:28:28 2005 +0200
+++ b/src/Pure/term.ML	Mon Jun 06 10:21:53 2005 +0200
@@ -791,7 +791,7 @@
   | add_typ_classes (TFree (_, S), cs) = S union cs
   | add_typ_classes (TVar (_, S), cs) = S union cs;
 
-fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins cs) Ts
+fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts
   | add_typ_tycons (_, cs) = cs;
 
 val add_term_classes = it_term_types add_typ_classes;
@@ -862,7 +862,7 @@
 (*Accumulates the TVars in a type, suppressing duplicates. *)
 fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
   | add_typ_tvars(TFree(_),vs) = vs
-  | add_typ_tvars(TVar(v),vs) = v ins vs;
+  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
 
 (*Accumulates the TFrees in a type, suppressing duplicates. *)
 fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
@@ -870,7 +870,7 @@
   | add_typ_tfree_names(TVar(_),fs) = fs;
 
 fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
-  | add_typ_tfrees(TFree(f),fs) = f ins fs
+  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
   | add_typ_tfrees(TVar(_),fs) = fs;
 
 fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
@@ -988,10 +988,10 @@
 fun foldl_types f = foldl_term_types (fn _ => f);
 
 (*collect variables*)
-val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
+val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
 val add_tvars = foldl_types add_tvarsT;
-val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
-val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
+val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
+val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
 
 (*collect variable names*)
 val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);