avoid polymorphic ins;
authorwenzelm
Mon Jun 06 10:21:53 2005 +0200 (2005-06-06)
changeset 1629497c9f2c1de3d
parent 16293 a920fe734a49
child 16295 cd7a83dae4f9
avoid polymorphic ins;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Mon Jun 06 09:28:28 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Mon Jun 06 10:21:53 2005 +0200
     1.3 @@ -791,7 +791,7 @@
     1.4    | add_typ_classes (TFree (_, S), cs) = S union cs
     1.5    | add_typ_classes (TVar (_, S), cs) = S union cs;
     1.6  
     1.7 -fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins cs) Ts
     1.8 +fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins_string cs) Ts
     1.9    | add_typ_tycons (_, cs) = cs;
    1.10  
    1.11  val add_term_classes = it_term_types add_typ_classes;
    1.12 @@ -862,7 +862,7 @@
    1.13  (*Accumulates the TVars in a type, suppressing duplicates. *)
    1.14  fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
    1.15    | add_typ_tvars(TFree(_),vs) = vs
    1.16 -  | add_typ_tvars(TVar(v),vs) = v ins vs;
    1.17 +  | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
    1.18  
    1.19  (*Accumulates the TFrees in a type, suppressing duplicates. *)
    1.20  fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
    1.21 @@ -870,7 +870,7 @@
    1.22    | add_typ_tfree_names(TVar(_),fs) = fs;
    1.23  
    1.24  fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
    1.25 -  | add_typ_tfrees(TFree(f),fs) = f ins fs
    1.26 +  | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
    1.27    | add_typ_tfrees(TVar(_),fs) = fs;
    1.28  
    1.29  fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
    1.30 @@ -988,10 +988,10 @@
    1.31  fun foldl_types f = foldl_term_types (fn _ => f);
    1.32  
    1.33  (*collect variables*)
    1.34 -val add_tvarsT = foldl_atyps (fn (vs, TVar v) => v ins vs | (vs, _) => vs);
    1.35 +val add_tvarsT = foldl_atyps (fn (vs, TVar v) => insert (op =) v vs | (vs, _) => vs);
    1.36  val add_tvars = foldl_types add_tvarsT;
    1.37 -val add_vars = foldl_aterms (fn (vs, Var v) => v ins vs | (vs, _) => vs);
    1.38 -val add_frees = foldl_aterms (fn (vs, Free v) => v ins vs | (vs, _) => vs);
    1.39 +val add_vars = foldl_aterms (fn (vs, Var v) => insert (op =) v vs | (vs, _) => vs);
    1.40 +val add_frees = foldl_aterms (fn (vs, Free v) => insert (op =) v vs | (vs, _) => vs);
    1.41  
    1.42  (*collect variable names*)
    1.43  val add_term_varnames = foldl_aterms (fn (xs, Var (x, _)) => ins_ix (x, xs) | (xs, _) => xs);