insert replacing ins ins_int ins_string
authorhaftmann
Wed Oct 04 14:17:38 2006 +0200 (2006-10-04)
changeset 20854f9cf9e62d11c
parent 20853 3ff5a2e05810
child 20855 9f60d493c8fe
insert replacing ins ins_int ins_string
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/Integ/presburger.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Tools/ATP/reduce_axiomsN.ML
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/function_package/context_tree.ML
src/HOL/Tools/refute.ML
src/HOL/Tools/res_atp.ML
src/HOL/Tools/res_atp_setup.ML
src/HOL/Tools/res_clause.ML
src/HOLCF/IOA/ABP/Check.ML
src/HOLCF/fixrec_package.ML
src/Provers/blast.ML
src/Provers/ind.ML
src/Pure/Proof/extraction.ML
src/Pure/Syntax/parser.ML
src/Pure/Syntax/type_ext.ML
src/Pure/Thy/thm_deps.ML
src/Pure/library.ML
src/Pure/term.ML
src/Pure/type_infer.ML
     1.1 --- a/src/HOL/Import/proof_kernel.ML	Wed Oct 04 14:14:33 2006 +0200
     1.2 +++ b/src/HOL/Import/proof_kernel.ML	Wed Oct 04 14:17:38 2006 +0200
     1.3 @@ -1222,13 +1222,13 @@
     1.4      let
     1.5  	fun add_consts (Const (c, _), cs) =
     1.6  	    (case c of
     1.7 -		 "op =" => "==" ins_string cs
     1.8 -	       | "op -->" => "==>" ins_string cs
     1.9 +		 "op =" => Library.insert (op =) "==" cs
    1.10 +	       | "op -->" => Library.insert (op =) "==>" cs
    1.11  	       | "All" => cs
    1.12  	       | "all" => cs
    1.13  	       | "op &" => cs
    1.14  	       | "Trueprop" => cs
    1.15 -	       | _ => c ins_string cs)
    1.16 +	       | _ => Library.insert (op =) c cs)
    1.17  	  | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
    1.18  	  | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
    1.19  	  | add_consts (_, cs) = cs
     2.1 --- a/src/HOL/Import/shuffler.ML	Wed Oct 04 14:14:33 2006 +0200
     2.2 +++ b/src/HOL/Import/shuffler.ML	Wed Oct 04 14:17:38 2006 +0200
     2.3 @@ -554,7 +554,7 @@
     2.4  	fun add_consts (Const (c, _), cs) =
     2.5  	    if c mem_string ignore
     2.6  	    then cs
     2.7 -	    else c ins_string cs
     2.8 +	    else insert (op =) c cs
     2.9  	  | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs))
    2.10  	  | add_consts (Abs (_, _, t), cs) = add_consts (t, cs)
    2.11  	  | add_consts (_, cs) = cs
    2.12 @@ -575,7 +575,7 @@
    2.13  		  val ignore_lhs = term_consts lhs \\ term_consts rhs
    2.14  		  val ignore_rhs = term_consts rhs \\ term_consts lhs
    2.15  	      in
    2.16 -		  foldr (op ins_string) cs (ignore_lhs @ ignore_rhs)
    2.17 +		  fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs)
    2.18  	      end)
    2.19  
    2.20  (* set_prop t thms tries to make a theorem with the proposition t from
     3.1 --- a/src/HOL/Integ/presburger.ML	Wed Oct 04 14:14:33 2006 +0200
     3.2 +++ b/src/HOL/Integ/presburger.ML	Wed Oct 04 14:17:38 2006 +0200
     3.3 @@ -104,7 +104,7 @@
     3.4  
     3.5  
     3.6  (* extract all the constants in a term*)
     3.7 -fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
     3.8 +fun add_term_typed_consts (Const (c, T), cs) = insert (op =) (c, T) cs
     3.9    | add_term_typed_consts (t $ u, cs) =
    3.10        add_term_typed_consts (t, add_term_typed_consts (u, cs))
    3.11    | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
     4.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Wed Oct 04 14:14:33 2006 +0200
     4.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Wed Oct 04 14:17:38 2006 +0200
     4.3 @@ -245,9 +245,9 @@
     4.4  (* it collects all free variables and tries to show       *)
     4.5  (* that the support of these free variables (op supports) *)
     4.6  (* the goal                                               *)
     4.7 -fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs
     4.8 -  | collect_vars i (v as Free _) vs = v ins vs
     4.9 -  | collect_vars i (v as Var _) vs = v ins vs
    4.10 +fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs
    4.11 +  | collect_vars i (v as Free _) vs = insert (op =) v vs
    4.12 +  | collect_vars i (v as Var _) vs = insert (op =) v vs
    4.13    | collect_vars i (Const _) vs = vs
    4.14    | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs
    4.15    | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs);
     5.1 --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Oct 04 14:14:33 2006 +0200
     5.2 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML	Wed Oct 04 14:17:38 2006 +0200
     5.3 @@ -65,7 +65,7 @@
     5.4  (*Add a const/type pair to the table, but a [] entry means a standard connective,
     5.5    which we ignore.*)
     5.6  fun add_const_typ_table ((c,ctyps), tab) =
     5.7 -  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => ctyps ins ctyps_list) 
     5.8 +  Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) 
     5.9      tab;
    5.10  
    5.11  (*Free variables are included, as well as constants, to handle locales*)
     6.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Wed Oct 04 14:14:33 2006 +0200
     6.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Wed Oct 04 14:17:38 2006 +0200
     6.3 @@ -104,7 +104,7 @@
     6.4  
     6.5  
     6.6  (* extract all the constants in a term*)
     6.7 -fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs
     6.8 +fun add_term_typed_consts (Const (c, T), cs) = insert (op =) (c, T) cs
     6.9    | add_term_typed_consts (t $ u, cs) =
    6.10        add_term_typed_consts (t, add_term_typed_consts (u, cs))
    6.11    | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs)
     7.1 --- a/src/HOL/Tools/function_package/context_tree.ML	Wed Oct 04 14:14:33 2006 +0200
     7.2 +++ b/src/HOL/Tools/function_package/context_tree.ML	Wed Oct 04 14:17:38 2006 +0200
     7.3 @@ -138,7 +138,7 @@
     7.4  
     7.5  (* FIXME: remove *)		
     7.6  fun add_context_varnames (Leaf _) = I
     7.7 -  | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (curry op ins_string o fst) fs o add_context_varnames st) sub
     7.8 +  | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (insert (op =) o fst) fs o add_context_varnames st) sub
     7.9    | add_context_varnames (RCall (_,st)) = add_context_varnames st
    7.10      
    7.11  
     8.1 --- a/src/HOL/Tools/refute.ML	Wed Oct 04 14:14:33 2006 +0200
     8.2 +++ b/src/HOL/Tools/refute.ML	Wed Oct 04 14:17:38 2006 +0200
     8.3 @@ -785,7 +785,7 @@
     8.4  									())
     8.5  							(* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *)
     8.6  							val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then
     8.7 -									T ins acc
     8.8 +									insert (op =) T acc
     8.9  								else
    8.10  									acc)
    8.11  							(* collect argument types *)
    8.12 @@ -796,9 +796,9 @@
    8.13  							acc_constrs
    8.14  						end
    8.15  					| NONE =>  (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *)
    8.16 -						T ins (foldr collect_types acc Ts))
    8.17 -				| TFree _                => T ins acc
    8.18 -				| TVar _                 => T ins acc)
    8.19 +						insert (op =) T (foldr collect_types acc Ts))
    8.20 +				| TFree _                => insert (op =) T acc
    8.21 +				| TVar _                 => insert (op =) T acc)
    8.22  	in
    8.23  		it_term_types collect_types (t, [])
    8.24  	end;
     9.1 --- a/src/HOL/Tools/res_atp.ML	Wed Oct 04 14:14:33 2006 +0200
     9.2 +++ b/src/HOL/Tools/res_atp.ML	Wed Oct 04 14:17:38 2006 +0200
     9.3 @@ -202,12 +202,12 @@
     9.4  exception FN_LG of term;
     9.5  
     9.6  fun fn_lg (t as Const(f,tp)) (lg,seen) = 
     9.7 -    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
     9.8 +    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
     9.9    | fn_lg (t as Free(f,tp)) (lg,seen) = 
    9.10 -    if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
    9.11 +    if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
    9.12    | fn_lg (t as Var(f,tp)) (lg,seen) =
    9.13 -    if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen)
    9.14 -  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
    9.15 +    if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen)
    9.16 +  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen)
    9.17    | fn_lg f _ = raise FN_LG(f); 
    9.18  
    9.19  
    9.20 @@ -226,10 +226,10 @@
    9.21  exception PRED_LG of term;
    9.22  
    9.23  fun pred_lg (t as Const(P,tp)) (lg,seen)= 
    9.24 -      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
    9.25 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) 
    9.26    | pred_lg (t as Free(P,tp)) (lg,seen) =
    9.27 -      if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
    9.28 -  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
    9.29 +      if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen)
    9.30 +  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
    9.31    | pred_lg P _ = raise PRED_LG(P);
    9.32  
    9.33  
    10.1 --- a/src/HOL/Tools/res_atp_setup.ML	Wed Oct 04 14:14:33 2006 +0200
    10.2 +++ b/src/HOL/Tools/res_atp_setup.ML	Wed Oct 04 14:17:38 2006 +0200
    10.3 @@ -180,13 +180,13 @@
    10.4  exception FN_LG of term;
    10.5  
    10.6  fun fn_lg (t as Const(f,tp)) (lg,seen) = 
    10.7 -    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
    10.8 +    if has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
    10.9    | fn_lg (t as Free(f,tp)) (lg,seen) = 
   10.10 -    if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) 
   10.11 +    if has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) 
   10.12    | fn_lg (t as Var(f,tp)) (lg,seen) =
   10.13 -    if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen)
   10.14 -    else (lg,t ins seen)
   10.15 -  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen)
   10.16 +    if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen)
   10.17 +    else (lg, insert (op =) t seen)
   10.18 +  | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg, insert (op =) t seen)
   10.19    | fn_lg f _ = raise FN_LG(f); 
   10.20  
   10.21  
   10.22 @@ -204,10 +204,10 @@
   10.23  exception PRED_LG of term;
   10.24  
   10.25  fun pred_lg (t as Const(P,tp)) (lg,seen)= 
   10.26 -    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) 
   10.27 +    if has_bool_arg tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen)
   10.28    | pred_lg (t as Free(P,tp)) (lg,seen) =
   10.29 -    if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen)
   10.30 -  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen)
   10.31 +    if has_bool_arg tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen)
   10.32 +  | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen)
   10.33    | pred_lg P _ = raise PRED_LG(P);
   10.34  
   10.35  
    11.1 --- a/src/HOL/Tools/res_clause.ML	Wed Oct 04 14:14:33 2006 +0200
    11.2 +++ b/src/HOL/Tools/res_clause.ML	Wed Oct 04 14:17:38 2006 +0200
    11.3 @@ -452,7 +452,7 @@
    11.4  
    11.5  fun get_tvar_strs [] = []
    11.6    | get_tvar_strs ((FOLTVar indx,s)::tss) = 
    11.7 -      (make_schematic_type_var indx) ins (get_tvar_strs tss)
    11.8 +      insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss)
    11.9    | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss
   11.10  
   11.11  (* check if a clause is first-order before making a conjecture clause*)
    12.1 --- a/src/HOLCF/IOA/ABP/Check.ML	Wed Oct 04 14:14:33 2006 +0200
    12.2 +++ b/src/HOLCF/IOA/ABP/Check.ML	Wed Oct 04 14:17:38 2006 +0200
    12.3 @@ -28,7 +28,7 @@
    12.4                                   string_of_s s; writeln"";
    12.5                                   string_of_a a; writeln"";
    12.6                                   string_of_s t;writeln"";writeln"" ));
    12.7 -                     if t mem checked then unchecked else t ins unchecked)
    12.8 +                     if t mem checked then unchecked else insert (op =) t unchecked)
    12.9                in Library.foldl check_sas (unchecked,nexts s a) end;
   12.10                val unchecked' = Library.foldl check_sa (unchecked,extacts @ intacts)
   12.11          in    (if s mem startsI then 
    13.1 --- a/src/HOLCF/fixrec_package.ML	Wed Oct 04 14:14:33 2006 +0200
    13.2 +++ b/src/HOLCF/fixrec_package.ML	Wed Oct 04 14:17:38 2006 +0200
    13.3 @@ -124,10 +124,10 @@
    13.4  (*********** monadic notation and pattern matching compilation ***********)
    13.5  (*************************************************************************)
    13.6  
    13.7 -fun add_names (Const(a,_), bs) = Sign.base_name a ins_string bs
    13.8 -  | add_names (Free(a,_) , bs) = a ins_string bs
    13.9 +fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs
   13.10 +  | add_names (Free(a,_) , bs) = insert (op =) a bs
   13.11    | add_names (f $ u     , bs) = add_names (f, add_names(u, bs))
   13.12 -  | add_names (Abs(a,_,t), bs) = add_names (t, a ins_string bs)
   13.13 +  | add_names (Abs(a,_,t), bs) = add_names (t, insert (op =) a bs)
   13.14    | add_names (_         , bs) = bs;
   13.15  
   13.16  fun add_terms ts xs = foldr add_names xs ts;
    14.1 --- a/src/Provers/blast.ML	Wed Oct 04 14:14:33 2006 +0200
    14.2 +++ b/src/Provers/blast.ML	Wed Oct 04 14:17:38 2006 +0200
    14.3 @@ -251,7 +251,7 @@
    14.4  (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
    14.5     (Bound 0) is loose at level 0 *)
    14.6  fun add_loose_bnos (Bound i, lev, js)   = if i<lev then js
    14.7 -                                          else  (i-lev) ins_int js
    14.8 +                                          else insert (op =) (i - lev) js
    14.9    | add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   14.10    | add_loose_bnos (f$t, lev, js)       =
   14.11                  add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
    15.1 --- a/src/Provers/ind.ML	Wed Oct 04 14:14:33 2006 +0200
    15.2 +++ b/src/Provers/ind.ML	Wed Oct 04 14:17:38 2006 +0200
    15.3 @@ -28,7 +28,7 @@
    15.4  
    15.5  fun add_term_frees thy =
    15.6  let fun add(tm, vars) = case tm of
    15.7 -	Free(v,T) => if Sign.typ_instance thy (T,aT) then v ins vars
    15.8 +	Free(v,T) => if Sign.typ_instance thy (T,aT) then insert (op =) v vars
    15.9  		     else vars
   15.10        | Abs (_,_,body) => add(body,vars)
   15.11        | rator$rand => add(rator, add(rand, vars))
    16.1 --- a/src/Pure/Proof/extraction.ML	Wed Oct 04 14:14:33 2006 +0200
    16.2 +++ b/src/Pure/Proof/extraction.ML	Wed Oct 04 14:17:38 2006 +0200
    16.3 @@ -378,7 +378,7 @@
    16.4        else
    16.5          {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
    16.6           realizers = realizers, defs = defs,
    16.7 -         expand = (name, prop_of thm) ins expand, prep = prep}) thy)
    16.8 +         expand = insert (op =) (name, prop_of thm) expand, prep = prep}) thy)
    16.9    end;
   16.10  
   16.11  val add_expand_thms = fold add_expand_thm;
    17.1 --- a/src/Pure/Syntax/parser.ML	Wed Oct 04 14:14:33 2006 +0200
    17.2 +++ b/src/Pure/Syntax/parser.ML	Wed Oct 04 14:17:38 2006 +0200
    17.3 @@ -76,7 +76,7 @@
    17.4        val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from =>
    17.5          let val old_tos = these (AList.lookup (op =) chains from) in
    17.6            if member (op =) old_tos lhs then (NONE, chains)
    17.7 -          else (SOME from, AList.update (op =) (from, lhs ins old_tos) chains)
    17.8 +          else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains)
    17.9          end;
   17.10  
   17.11        (*propagate new chain in lookahead and lambda lists;
   17.12 @@ -336,7 +336,7 @@
   17.13  
   17.14                              val tk_prods' =
   17.15                                if not lambda then p :: tk_prods
   17.16 -                              else p ins tk_prods;
   17.17 +                              else insert (op =) p tk_prods;
   17.18                                        (*if production depends on lambda NT we
   17.19                                          have to look for duplicates*)
   17.20                           in
    18.1 --- a/src/Pure/Syntax/type_ext.ML	Wed Oct 04 14:14:33 2006 +0200
    18.2 +++ b/src/Pure/Syntax/type_ext.ML	Wed Oct 04 14:17:38 2006 +0200
    18.3 @@ -55,13 +55,13 @@
    18.4  fun raw_term_sorts tm =
    18.5    let
    18.6      fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env =
    18.7 -          ((x, ~1), sort_of_term cs) ins env
    18.8 +          insert (op =) ((x, ~1), sort_of_term cs) env
    18.9        | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env =
   18.10 -          ((x, ~1), sort_of_term cs) ins env
   18.11 +          insert (op =) ((x, ~1), sort_of_term cs) env
   18.12        | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env =
   18.13 -          (xi, sort_of_term cs) ins env
   18.14 +          insert (op =) (xi, sort_of_term cs) env
   18.15        | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env =
   18.16 -          (xi, sort_of_term cs) ins env
   18.17 +          insert (op =) (xi, sort_of_term cs) env
   18.18        | add_env (Abs (_, _, t)) env = add_env t env
   18.19        | add_env (t1 $ t2) env = add_env t1 (add_env t2 env)
   18.20        | add_env _ env = env;
    19.1 --- a/src/Pure/Thy/thm_deps.ML	Wed Oct 04 14:14:33 2006 +0200
    19.2 +++ b/src/Pure/Thy/thm_deps.ML	Wed Oct 04 14:17:38 2006 +0200
    19.3 @@ -59,9 +59,9 @@
    19.4                  {name = Sign.base_name name, ID = name,
    19.5                   dir = space_implode "/" (session @ prefx),
    19.6                   unfold = false, path = "", parents = parents'}) gra',
    19.7 -               name ins parents)
    19.8 +               insert (op =) name parents)
    19.9              end
   19.10 -          else (gra, name ins parents)
   19.11 +          else (gra, insert (op =) name parents)
   19.12          else
   19.13            make_deps_graph prf' (gra, parents)
   19.14        end);
    20.1 --- a/src/Pure/library.ML	Wed Oct 04 14:14:33 2006 +0200
    20.2 +++ b/src/Pure/library.ML	Wed Oct 04 14:17:38 2006 +0200
    20.3 @@ -12,7 +12,7 @@
    20.4  infix 3 o oo ooo oooo;
    20.5  
    20.6  infix 4 ~~ upto downto;
    20.7 -infix orf andf \ \\ ins ins_string ins_int mem mem_int mem_string union union_int
    20.8 +infix orf andf \ \\ mem mem_int mem_string union union_int
    20.9    union_string inter inter_int inter_string subset subset_int subset_string;
   20.10  
   20.11  signature BASIC_LIBRARY =
   20.12 @@ -201,9 +201,6 @@
   20.13    val mem: ''a * ''a list -> bool
   20.14    val mem_int: int * int list -> bool
   20.15    val mem_string: string * string list -> bool
   20.16 -  val ins: ''a * ''a list -> ''a list
   20.17 -  val ins_int: int * int list -> int list
   20.18 -  val ins_string: string * string list -> string list
   20.19    val union: ''a list * ''a list -> ''a list
   20.20    val union_int: int list * int list -> int list
   20.21    val union_string: string list * string list -> string list
   20.22 @@ -959,25 +956,21 @@
   20.23  fun (x: int) mem_int xs = member (op =) xs x;
   20.24  fun (x: string) mem_string xs = member (op =) xs x;
   20.25  
   20.26 -fun x ins xs = insert (op =) x xs;
   20.27 -fun (x: int) ins_int xs = insert (op =) x xs;
   20.28 -fun (x: string) ins_string xs = insert (op =) x xs;
   20.29 -
   20.30  
   20.31  (*union of sets represented as lists: no repetitions*)
   20.32  fun xs union [] = xs
   20.33    | [] union ys = ys
   20.34 -  | (x :: xs) union ys = xs union (x ins ys);
   20.35 +  | (x :: xs) union ys = xs union (insert (op =) x ys);
   20.36  
   20.37  (*union of sets, optimized version for ints*)
   20.38  fun (xs:int list) union_int [] = xs
   20.39    | [] union_int ys = ys
   20.40 -  | (x :: xs) union_int ys = xs union_int (x ins_int ys);
   20.41 +  | (x :: xs) union_int ys = xs union_int (insert (op =) x ys);
   20.42  
   20.43  (*union of sets, optimized version for strings*)
   20.44  fun (xs:string list) union_string [] = xs
   20.45    | [] union_string ys = ys
   20.46 -  | (x :: xs) union_string ys = xs union_string (x ins_string ys);
   20.47 +  | (x :: xs) union_string ys = xs union_string (insert (op =) x ys);
   20.48  
   20.49  (*generalized union*)
   20.50  fun gen_union eq (xs, []) = xs
    21.1 --- a/src/Pure/term.ML	Wed Oct 04 14:14:33 2006 +0200
    21.2 +++ b/src/Pure/term.ML	Wed Oct 04 14:17:38 2006 +0200
    21.3 @@ -728,7 +728,7 @@
    21.4  (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond.
    21.5     (Bound 0) is loose at level 0 *)
    21.6  fun add_loose_bnos (Bound i, lev, js) =
    21.7 -        if i<lev then js  else  (i-lev) ins_int js
    21.8 +        if i<lev then js else insert (op =) (i - lev) js
    21.9    | add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
   21.10    | add_loose_bnos (f$t, lev, js) =
   21.11          add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
   21.12 @@ -1043,15 +1043,15 @@
   21.13  (** TFrees and TVars **)
   21.14  
   21.15  (*Accumulates the names of Frees in the term, suppressing duplicates.*)
   21.16 -fun add_term_free_names (Free(a,_), bs) = a ins_string bs
   21.17 +fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
   21.18    | add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
   21.19    | add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
   21.20    | add_term_free_names (_, bs) = bs;
   21.21  
   21.22  (*Accumulates the names in the term, suppressing duplicates.
   21.23    Includes Frees and Consts.  For choosing unambiguous bound var names.*)
   21.24 -fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
   21.25 -  | add_term_names (Free(a,_), bs) = a ins_string bs
   21.26 +fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
   21.27 +  | add_term_names (Free(a,_), bs) = insert (op =) a bs
   21.28    | add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
   21.29    | add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
   21.30    | add_term_names (_, bs) = bs;
   21.31 @@ -1063,7 +1063,7 @@
   21.32  
   21.33  (*Accumulates the TFrees in a type, suppressing duplicates. *)
   21.34  fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
   21.35 -  | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
   21.36 +  | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
   21.37    | add_typ_tfree_names(TVar(_),fs) = fs;
   21.38  
   21.39  fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
   21.40 @@ -1071,8 +1071,8 @@
   21.41    | add_typ_tfrees(TVar(_),fs) = fs;
   21.42  
   21.43  fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
   21.44 -  | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
   21.45 -  | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
   21.46 +  | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
   21.47 +  | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
   21.48  
   21.49  (*Accumulates the TVars in a term, suppressing duplicates. *)
   21.50  val add_term_tvars = it_term_types add_typ_tvars;
    22.1 --- a/src/Pure/type_infer.ML	Wed Oct 04 14:14:33 2006 +0200
    22.2 +++ b/src/Pure/type_infer.ML	Wed Oct 04 14:17:38 2006 +0200
    22.3 @@ -192,7 +192,7 @@
    22.4  (* add_parms *)
    22.5  
    22.6  fun add_parmsT (PType (_, Ts)) rs = fold add_parmsT Ts rs
    22.7 -  | add_parmsT (Link (r as ref (Param _))) rs = r ins rs
    22.8 +  | add_parmsT (Link (r as ref (Param _))) rs = insert (op =) r rs
    22.9    | add_parmsT (Link (ref T)) rs = add_parmsT T rs
   22.10    | add_parmsT _ rs = rs;
   22.11