--- 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
--- 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
--- 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)
--- 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);
--- 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*)
--- 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)
--- 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
--- 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;
--- 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);
--- 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);
--- 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*)
--- 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
--- 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;
--- 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<lev then js
- else (i-lev) ins_int js
+ else insert (op =) (i - lev) js
| add_loose_bnos (Abs (_,t), lev, js) = add_loose_bnos (t, lev+1, js)
| add_loose_bnos (f$t, lev, js) =
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
--- a/src/Provers/ind.ML Wed Oct 04 14:14:33 2006 +0200
+++ b/src/Provers/ind.ML Wed Oct 04 14:17:38 2006 +0200
@@ -28,7 +28,7 @@
fun add_term_frees thy =
let fun add(tm, vars) = case tm of
- Free(v,T) => 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))
--- 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;
--- 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
--- 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;
--- 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);
--- 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
--- 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<lev then js else (i-lev) ins_int js
+ if i<lev then js else insert (op =) (i - lev) js
| add_loose_bnos (Abs (_,_,t), lev, js) = add_loose_bnos (t, lev+1, js)
| add_loose_bnos (f$t, lev, js) =
add_loose_bnos (f, lev, add_loose_bnos (t, lev, js))
@@ -1043,15 +1043,15 @@
(** TFrees and TVars **)
(*Accumulates the names of Frees in the term, suppressing duplicates.*)
-fun add_term_free_names (Free(a,_), bs) = a ins_string bs
+fun add_term_free_names (Free(a,_), bs) = insert (op =) a bs
| add_term_free_names (f$u, bs) = add_term_free_names (f, add_term_free_names(u, bs))
| add_term_free_names (Abs(_,_,t), bs) = add_term_free_names(t,bs)
| add_term_free_names (_, bs) = bs;
(*Accumulates the names in the term, suppressing duplicates.
Includes Frees and Consts. For choosing unambiguous bound var names.*)
-fun add_term_names (Const(a,_), bs) = NameSpace.base a ins_string bs
- | add_term_names (Free(a,_), bs) = a ins_string bs
+fun add_term_names (Const(a,_), bs) = insert (op =) (NameSpace.base a) bs
+ | add_term_names (Free(a,_), bs) = insert (op =) a bs
| add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs))
| add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs)
| add_term_names (_, bs) = bs;
@@ -1063,7 +1063,7 @@
(*Accumulates the TFrees in a type, suppressing duplicates. *)
fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
- | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
+ | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
| add_typ_tfree_names(TVar(_),fs) = fs;
fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
@@ -1071,8 +1071,8 @@
| add_typ_tfrees(TVar(_),fs) = fs;
fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
- | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
- | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
+ | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
+ | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
(*Accumulates the TVars in a term, suppressing duplicates. *)
val add_term_tvars = it_term_types add_typ_tvars;
--- a/src/Pure/type_infer.ML Wed Oct 04 14:14:33 2006 +0200
+++ b/src/Pure/type_infer.ML Wed Oct 04 14:17:38 2006 +0200
@@ -192,7 +192,7 @@
(* add_parms *)
fun add_parmsT (PType (_, Ts)) rs = fold add_parmsT Ts rs
- | add_parmsT (Link (r as ref (Param _))) rs = r ins rs
+ | add_parmsT (Link (r as ref (Param _))) rs = insert (op =) r rs
| add_parmsT (Link (ref T)) rs = add_parmsT T rs
| add_parmsT _ rs = rs;