# HG changeset patch # User haftmann # Date 1159964258 -7200 # Node ID f9cf9e62d11cb150552e0eec04409b3ffa2e3e05 # Parent 3ff5a2e058104680c93cfa4ee7bdea8988e46746 insert replacing ins ins_int ins_string diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Import/proof_kernel.ML Wed Oct 04 14:17:38 2006 +0200 @@ -1222,13 +1222,13 @@ let fun add_consts (Const (c, _), cs) = (case c of - "op =" => "==" ins_string cs - | "op -->" => "==>" ins_string cs + "op =" => Library.insert (op =) "==" cs + | "op -->" => Library.insert (op =) "==>" cs | "All" => cs | "all" => cs | "op &" => cs | "Trueprop" => cs - | _ => c ins_string cs) + | _ => Library.insert (op =) c cs) | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) | add_consts (Abs (_, _, t), cs) = add_consts (t, cs) | add_consts (_, cs) = cs diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Import/shuffler.ML Wed Oct 04 14:17:38 2006 +0200 @@ -554,7 +554,7 @@ fun add_consts (Const (c, _), cs) = if c mem_string ignore then cs - else c ins_string cs + else insert (op =) c cs | add_consts (t $ u, cs) = add_consts (t, add_consts (u, cs)) | add_consts (Abs (_, _, t), cs) = add_consts (t, cs) | add_consts (_, cs) = cs @@ -575,7 +575,7 @@ val ignore_lhs = term_consts lhs \\ term_consts rhs val ignore_rhs = term_consts rhs \\ term_consts lhs in - foldr (op ins_string) cs (ignore_lhs @ ignore_rhs) + fold_rev (insert (op =)) cs (ignore_lhs @ ignore_rhs) end) (* set_prop t thms tries to make a theorem with the proposition t from diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Integ/presburger.ML --- a/src/HOL/Integ/presburger.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Integ/presburger.ML Wed Oct 04 14:17:38 2006 +0200 @@ -104,7 +104,7 @@ (* extract all the constants in a term*) -fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs +fun add_term_typed_consts (Const (c, T), cs) = insert (op =) (c, T) cs | add_term_typed_consts (t $ u, cs) = add_term_typed_consts (t, add_term_typed_consts (u, cs)) | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs) diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Wed Oct 04 14:17:38 2006 +0200 @@ -245,9 +245,9 @@ (* it collects all free variables and tries to show *) (* that the support of these free variables (op supports) *) (* the goal *) -fun collect_vars i (Bound j) vs = if j < i then vs else Bound (j - i) ins vs - | collect_vars i (v as Free _) vs = v ins vs - | collect_vars i (v as Var _) vs = v ins vs +fun collect_vars i (Bound j) vs = if j < i then vs else insert (op =) (Bound (j - i)) vs + | collect_vars i (v as Free _) vs = insert (op =) v vs + | collect_vars i (v as Var _) vs = insert (op =) v vs | collect_vars i (Const _) vs = vs | collect_vars i (Abs (_, _, t)) vs = collect_vars (i+1) t vs | collect_vars i (t $ u) vs = collect_vars i u (collect_vars i t vs); diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Tools/ATP/reduce_axiomsN.ML --- a/src/HOL/Tools/ATP/reduce_axiomsN.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Tools/ATP/reduce_axiomsN.ML Wed Oct 04 14:17:38 2006 +0200 @@ -65,7 +65,7 @@ (*Add a const/type pair to the table, but a [] entry means a standard connective, which we ignore.*) fun add_const_typ_table ((c,ctyps), tab) = - Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => ctyps ins ctyps_list) + Symtab.map_default (c, [ctyps]) (fn [] => [] | ctyps_list => insert (op =) ctyps ctyps_list) tab; (*Free variables are included, as well as constants, to handle locales*) diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Tools/Presburger/presburger.ML --- a/src/HOL/Tools/Presburger/presburger.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Tools/Presburger/presburger.ML Wed Oct 04 14:17:38 2006 +0200 @@ -104,7 +104,7 @@ (* extract all the constants in a term*) -fun add_term_typed_consts (Const (c, T), cs) = (c,T) ins cs +fun add_term_typed_consts (Const (c, T), cs) = insert (op =) (c, T) cs | add_term_typed_consts (t $ u, cs) = add_term_typed_consts (t, add_term_typed_consts (u, cs)) | add_term_typed_consts (Abs (_, _, t), cs) = add_term_typed_consts (t, cs) diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Tools/function_package/context_tree.ML --- a/src/HOL/Tools/function_package/context_tree.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Tools/function_package/context_tree.ML Wed Oct 04 14:17:38 2006 +0200 @@ -138,7 +138,7 @@ (* FIXME: remove *) fun add_context_varnames (Leaf _) = I - | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (curry op ins_string o fst) fs o add_context_varnames st) sub + | add_context_varnames (Cong (_, _, _, sub)) = fold (fn (fs, _, st) => fold (insert (op =) o fst) fs o add_context_varnames st) sub | add_context_varnames (RCall (_,st)) = add_context_varnames st diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Tools/refute.ML --- a/src/HOL/Tools/refute.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Tools/refute.ML Wed Oct 04 14:17:38 2006 +0200 @@ -785,7 +785,7 @@ ()) (* if the current type is a recursive IDT (i.e. a depth is required), add it to 'acc' *) val acc' = (if Library.exists (fn (_, ds) => Library.exists DatatypeAux.is_rec_type ds) constrs then - T ins acc + insert (op =) T acc else acc) (* collect argument types *) @@ -796,9 +796,9 @@ acc_constrs end | NONE => (* not an inductive datatype, e.g. defined via "typedef" or "typedecl" *) - T ins (foldr collect_types acc Ts)) - | TFree _ => T ins acc - | TVar _ => T ins acc) + insert (op =) T (foldr collect_types acc Ts)) + | TFree _ => insert (op =) T acc + | TVar _ => insert (op =) T acc) in it_term_types collect_types (t, []) end; diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Tools/res_atp.ML --- a/src/HOL/Tools/res_atp.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Tools/res_atp.ML Wed Oct 04 14:17:38 2006 +0200 @@ -202,12 +202,12 @@ exception FN_LG of term; fun fn_lg (t as Const(f,tp)) (lg,seen) = - if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) + if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) | fn_lg (t as Free(f,tp)) (lg,seen) = - if is_hol_fn tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) + if is_hol_fn tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) | fn_lg (t as Var(f,tp)) (lg,seen) = - if is_hol_fn tp then (upgrade_lg HOL lg,t ins seen) else (lg,t ins seen) - | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen) + if is_hol_fn tp then (upgrade_lg HOL lg,insert (op =) t seen) else (lg,insert (op =) t seen) + | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,insert (op =) t seen) | fn_lg f _ = raise FN_LG(f); @@ -226,10 +226,10 @@ exception PRED_LG of term; fun pred_lg (t as Const(P,tp)) (lg,seen)= - if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) + if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) | pred_lg (t as Free(P,tp)) (lg,seen) = - if is_hol_pred tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) - | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen) + if is_hol_pred tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) + | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen) | pred_lg P _ = raise PRED_LG(P); diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Tools/res_atp_setup.ML --- a/src/HOL/Tools/res_atp_setup.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Tools/res_atp_setup.ML Wed Oct 04 14:17:38 2006 +0200 @@ -180,13 +180,13 @@ exception FN_LG of term; fun fn_lg (t as Const(f,tp)) (lg,seen) = - if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) + if has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) | fn_lg (t as Free(f,tp)) (lg,seen) = - if has_bool tp then (upgrade_lg HOL lg, t ins seen) else (lg, t ins seen) + if has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) | fn_lg (t as Var(f,tp)) (lg,seen) = - if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg,t ins seen) - else (lg,t ins seen) - | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg,t ins seen) + if is_fn_tp tp orelse has_bool tp then (upgrade_lg HOL lg, insert (op =) t seen) + else (lg, insert (op =) t seen) + | fn_lg (t as Abs(_,_,_)) (lg,seen) = (upgrade_lg HOLC lg, insert (op =) t seen) | fn_lg f _ = raise FN_LG(f); @@ -204,10 +204,10 @@ exception PRED_LG of term; fun pred_lg (t as Const(P,tp)) (lg,seen)= - if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) + if has_bool_arg tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg, insert (op =) t seen) | pred_lg (t as Free(P,tp)) (lg,seen) = - if has_bool_arg tp then (upgrade_lg HOL lg, t ins seen) else (lg,t ins seen) - | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, t ins seen) + if has_bool_arg tp then (upgrade_lg HOL lg, insert (op =) t seen) else (lg,insert (op =) t seen) + | pred_lg (t as Var(_,_)) (lg,seen) = (upgrade_lg HOL lg, insert (op =) t seen) | pred_lg P _ = raise PRED_LG(P); diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOL/Tools/res_clause.ML --- a/src/HOL/Tools/res_clause.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOL/Tools/res_clause.ML Wed Oct 04 14:17:38 2006 +0200 @@ -452,7 +452,7 @@ fun get_tvar_strs [] = [] | get_tvar_strs ((FOLTVar indx,s)::tss) = - (make_schematic_type_var indx) ins (get_tvar_strs tss) + insert (op =) (make_schematic_type_var indx) (get_tvar_strs tss) | get_tvar_strs((FOLTFree x,s)::tss) = get_tvar_strs tss (* check if a clause is first-order before making a conjecture clause*) diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOLCF/IOA/ABP/Check.ML --- a/src/HOLCF/IOA/ABP/Check.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOLCF/IOA/ABP/Check.ML Wed Oct 04 14:17:38 2006 +0200 @@ -28,7 +28,7 @@ string_of_s s; writeln""; string_of_a a; writeln""; string_of_s t;writeln"";writeln"" )); - if t mem checked then unchecked else t ins unchecked) + if t mem checked then unchecked else insert (op =) t unchecked) in Library.foldl check_sas (unchecked,nexts s a) end; val unchecked' = Library.foldl check_sa (unchecked,extacts @ intacts) in (if s mem startsI then diff -r 3ff5a2e05810 -r f9cf9e62d11c src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/HOLCF/fixrec_package.ML Wed Oct 04 14:17:38 2006 +0200 @@ -124,10 +124,10 @@ (*********** monadic notation and pattern matching compilation ***********) (*************************************************************************) -fun add_names (Const(a,_), bs) = Sign.base_name a ins_string bs - | add_names (Free(a,_) , bs) = a ins_string bs +fun add_names (Const(a,_), bs) = insert (op =) (Sign.base_name a) bs + | add_names (Free(a,_) , bs) = insert (op =) a bs | add_names (f $ u , bs) = add_names (f, add_names(u, bs)) - | add_names (Abs(a,_,t), bs) = add_names (t, a ins_string bs) + | add_names (Abs(a,_,t), bs) = add_names (t, insert (op =) a bs) | add_names (_ , bs) = bs; fun add_terms ts xs = foldr add_names xs ts; diff -r 3ff5a2e05810 -r f9cf9e62d11c src/Provers/blast.ML --- a/src/Provers/blast.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/Provers/blast.ML Wed Oct 04 14:17:38 2006 +0200 @@ -251,7 +251,7 @@ (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. (Bound 0) is loose at level 0 *) fun add_loose_bnos (Bound i, lev, js) = if i if Sign.typ_instance thy (T,aT) then v ins vars + Free(v,T) => if Sign.typ_instance thy (T,aT) then insert (op =) v vars else vars | Abs (_,_,body) => add(body,vars) | rator$rand => add(rator, add(rand, vars)) diff -r 3ff5a2e05810 -r f9cf9e62d11c src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/Pure/Proof/extraction.ML Wed Oct 04 14:17:38 2006 +0200 @@ -378,7 +378,7 @@ else {realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types, realizers = realizers, defs = defs, - expand = (name, prop_of thm) ins expand, prep = prep}) thy) + expand = insert (op =) (name, prop_of thm) expand, prep = prep}) thy) end; val add_expand_thms = fold add_expand_thm; diff -r 3ff5a2e05810 -r f9cf9e62d11c src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/Pure/Syntax/parser.ML Wed Oct 04 14:17:38 2006 +0200 @@ -76,7 +76,7 @@ val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from => let val old_tos = these (AList.lookup (op =) chains from) in if member (op =) old_tos lhs then (NONE, chains) - else (SOME from, AList.update (op =) (from, lhs ins old_tos) chains) + else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains) end; (*propagate new chain in lookahead and lambda lists; @@ -336,7 +336,7 @@ val tk_prods' = if not lambda then p :: tk_prods - else p ins tk_prods; + else insert (op =) p tk_prods; (*if production depends on lambda NT we have to look for duplicates*) in diff -r 3ff5a2e05810 -r f9cf9e62d11c src/Pure/Syntax/type_ext.ML --- a/src/Pure/Syntax/type_ext.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/Pure/Syntax/type_ext.ML Wed Oct 04 14:17:38 2006 +0200 @@ -55,13 +55,13 @@ fun raw_term_sorts tm = let fun add_env (Const ("_ofsort", _) $ Free (x, _) $ cs) env = - ((x, ~1), sort_of_term cs) ins env + insert (op =) ((x, ~1), sort_of_term cs) env | add_env (Const ("_ofsort", _) $ (Const ("_tfree",_) $ Free (x, _)) $ cs) env = - ((x, ~1), sort_of_term cs) ins env + insert (op =) ((x, ~1), sort_of_term cs) env | add_env (Const ("_ofsort", _) $ Var (xi, _) $ cs) env = - (xi, sort_of_term cs) ins env + insert (op =) (xi, sort_of_term cs) env | add_env (Const ("_ofsort", _) $ (Const ("_tvar",_) $ Var (xi, _)) $ cs) env = - (xi, sort_of_term cs) ins env + insert (op =) (xi, sort_of_term cs) env | add_env (Abs (_, _, t)) env = add_env t env | add_env (t1 $ t2) env = add_env t1 (add_env t2 env) | add_env _ env = env; diff -r 3ff5a2e05810 -r f9cf9e62d11c src/Pure/Thy/thm_deps.ML --- a/src/Pure/Thy/thm_deps.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/Pure/Thy/thm_deps.ML Wed Oct 04 14:17:38 2006 +0200 @@ -59,9 +59,9 @@ {name = Sign.base_name name, ID = name, dir = space_implode "/" (session @ prefx), unfold = false, path = "", parents = parents'}) gra', - name ins parents) + insert (op =) name parents) end - else (gra, name ins parents) + else (gra, insert (op =) name parents) else make_deps_graph prf' (gra, parents) end); diff -r 3ff5a2e05810 -r f9cf9e62d11c src/Pure/library.ML --- a/src/Pure/library.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/Pure/library.ML Wed Oct 04 14:17:38 2006 +0200 @@ -12,7 +12,7 @@ infix 3 o oo ooo oooo; infix 4 ~~ upto downto; -infix orf andf \ \\ ins ins_string ins_int mem mem_int mem_string union union_int +infix orf andf \ \\ mem mem_int mem_string union union_int union_string inter inter_int inter_string subset subset_int subset_string; signature BASIC_LIBRARY = @@ -201,9 +201,6 @@ val mem: ''a * ''a list -> bool val mem_int: int * int list -> bool val mem_string: string * string list -> bool - val ins: ''a * ''a list -> ''a list - val ins_int: int * int list -> int list - val ins_string: string * string list -> string list val union: ''a list * ''a list -> ''a list val union_int: int list * int list -> int list val union_string: string list * string list -> string list @@ -959,25 +956,21 @@ fun (x: int) mem_int xs = member (op =) xs x; fun (x: string) mem_string xs = member (op =) xs x; -fun x ins xs = insert (op =) x xs; -fun (x: int) ins_int xs = insert (op =) x xs; -fun (x: string) ins_string xs = insert (op =) x xs; - (*union of sets represented as lists: no repetitions*) fun xs union [] = xs | [] union ys = ys - | (x :: xs) union ys = xs union (x ins ys); + | (x :: xs) union ys = xs union (insert (op =) x ys); (*union of sets, optimized version for ints*) fun (xs:int list) union_int [] = xs | [] union_int ys = ys - | (x :: xs) union_int ys = xs union_int (x ins_int ys); + | (x :: xs) union_int ys = xs union_int (insert (op =) x ys); (*union of sets, optimized version for strings*) fun (xs:string list) union_string [] = xs | [] union_string ys = ys - | (x :: xs) union_string ys = xs union_string (x ins_string ys); + | (x :: xs) union_string ys = xs union_string (insert (op =) x ys); (*generalized union*) fun gen_union eq (xs, []) = xs diff -r 3ff5a2e05810 -r f9cf9e62d11c src/Pure/term.ML --- a/src/Pure/term.ML Wed Oct 04 14:14:33 2006 +0200 +++ b/src/Pure/term.ML Wed Oct 04 14:17:38 2006 +0200 @@ -728,7 +728,7 @@ (*Accumulate all 'loose' bound vars referring to level 'lev' or beyond. (Bound 0) is loose at level 0 *) fun add_loose_bnos (Bound i, lev, js) = - if i