--- a/src/HOL/Import/hol4rews.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/HOL/Import/hol4rews.ML Fri Feb 03 23:12:28 2006 +0100
@@ -264,7 +264,7 @@
val _ = message "Adding HOL4 rewrite"
val th1 = th RS eq_reflection
val current_rews = HOL4Rewrites.get thy
- val new_rews = gen_ins Thm.eq_thm (th1,current_rews)
+ val new_rews = insert Thm.eq_thm th1 current_rews
val updated_thy = HOL4Rewrites.put new_rews thy
in
(Context.Theory updated_thy,th1)
--- a/src/HOL/Tools/inductive_package.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML Fri Feb 03 23:12:28 2006 +0100
@@ -148,8 +148,8 @@
(* attributes *)
-val mono_add = Thm.declaration_attribute (map_monos o Drule.add_rules o mk_mono);
-val mono_del = Thm.declaration_attribute (map_monos o Drule.del_rules o mk_mono);
+val mono_add = Thm.declaration_attribute (map_monos o fold Drule.add_rule o mk_mono);
+val mono_del = Thm.declaration_attribute (map_monos o fold Drule.del_rule o mk_mono);
--- a/src/HOL/Tools/specification_package.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/HOL/Tools/specification_package.ML Fri Feb 03 23:12:28 2006 +0100
@@ -95,7 +95,7 @@
fun collect_consts ( t $ u,tms) = collect_consts (u,collect_consts (t,tms))
| collect_consts ( Abs(_,_,t),tms) = collect_consts (t,tms)
- | collect_consts (tm as Const _,tms) = gen_ins (op aconv) (tm,tms)
+ | collect_consts (tm as Const _,tms) = insert (op aconv) tm tms
| collect_consts ( _,tms) = tms
(* Complementing Type.varify... *)
--- a/src/Pure/General/graph.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/General/graph.ML Fri Feb 03 23:12:28 2006 +0100
@@ -55,9 +55,7 @@
val eq_key = equal EQUAL o Key.ord;
-infix mem_key;
-val op mem_key = gen_mem eq_key;
-
+val member_key = member eq_key;
val remove_key = remove eq_key;
@@ -68,11 +66,8 @@
val empty_keys = Table.empty: keys;
-infix mem_keys;
-fun x mem_keys tab = Table.defined (tab: keys) x;
-
-infix ins_keys;
-fun x ins_keys tab = Table.insert (K true) (x, ()) (tab: keys);
+fun member_keys tab = Table.defined (tab: keys);
+fun insert_keys x tab = Table.insert (K true) (x, ()) (tab: keys);
(* graphs *)
@@ -126,8 +121,8 @@
fun reachable next xs =
let
fun reach x (rs, R) =
- if x mem_keys R then (rs, R)
- else apfst (cons x) (fold reach (next x) (rs, x ins_keys R))
+ if member_keys R x then (rs, R)
+ else apfst (cons x) (fold reach (next x) (rs, insert_keys x R))
in fold_map (fn x => reach x o pair []) xs empty_keys end;
(*immediate*)
@@ -161,7 +156,7 @@
val (_, X) = reachable (imm_succs G) [x];
fun paths ps p =
if not (null ps) andalso eq_key (p, x) then [p :: ps]
- else if p mem_keys X andalso not (p mem_key ps)
+ else if member_keys X p andalso not (member_key ps p)
then List.concat (map (paths (p :: ps)) (imm_preds G p))
else [];
in paths [] y end;
@@ -184,7 +179,7 @@
(* edges *)
-fun is_edge G (x, y) = y mem_key imm_succs G x handle UNDEF _ => false;
+fun is_edge G (x, y) = member_key (imm_succs G x) y handle UNDEF _ => false;
fun add_edge (x, y) G =
if is_edge G (x, y) then G
--- a/src/Pure/Isar/context_rules.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML Fri Feb 03 23:12:28 2006 +0100
@@ -104,9 +104,9 @@
Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
let
val wrappers =
- (gen_merge_lists' (eq_snd (op =)) ws1 ws2, gen_merge_lists' (eq_snd (op =)) ws1' ws2');
- val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) =>
- k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) rules1 rules2;
+ (Library.merge (eq_snd (op =)) (ws1, ws2), Library.merge (eq_snd (op =)) (ws1', ws2'));
+ val rules = Library.merge (fn ((_, (k1, th1)), (_, (k2, th2))) =>
+ k1 = k2 andalso Drule.eq_thm_prop (th1, th2)) (rules1, rules2);
val next = ~ (length rules);
val netpairs = Library.foldl (fn (nps, (n, (w, ((i, b), th)))) =>
nth_map i (curry insert_tagged_brl ((w, n), (b, th))) nps)
--- a/src/Pure/Isar/method.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/Isar/method.ML Fri Feb 03 23:12:28 2006 +0100
@@ -325,8 +325,8 @@
val ps = Logic.strip_assums_hyp g;
val c = Logic.strip_assums_concl g;
in
- if gen_mem (fn ((ps1, c1), (ps2, c2)) =>
- c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) ((ps, c), gs) then no_tac
+ if member (fn ((ps1, c1), (ps2, c2)) =>
+ c1 aconv c2 andalso gen_eq_set op aconv ps1 ps2) gs (ps, c) then no_tac
else (step_tac ctxt THEN_ALL_NEW intprover_tac ctxt ((ps, c) :: gs) (d + 1) lim) i
end);
--- a/src/Pure/Isar/net_rules.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/Isar/net_rules.ML Fri Feb 03 23:12:28 2006 +0100
@@ -50,7 +50,7 @@
(Net.insert_term (K false) (index rule, (next, rule)) net);
fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
- let val rules = Library.gen_merge_lists' eq rules1 rules2
+ let val rules = Library.merge eq (rules1, rules2)
in fold_rev add rules (init eq index) end;
fun delete rule (rs as Rules {eq, index, rules, next, net}) =
--- a/src/Pure/Proof/extraction.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/Proof/extraction.ML Fri Feb 03 23:12:28 2006 +0100
@@ -374,7 +374,7 @@
typeof_eqns = add_rule (([],
Logic.dest_equals (prop_of (Drule.abs_def thm))), typeof_eqns),
types = types,
- realizers = realizers, defs = gen_ins eq_thm (thm, defs),
+ realizers = realizers, defs = insert eq_thm thm defs,
expand = expand, prep = prep}
else
{realizes_eqns = realizes_eqns, typeof_eqns = typeof_eqns, types = types,
--- a/src/Pure/Syntax/syntax.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML Fri Feb 03 23:12:28 2006 +0100
@@ -218,8 +218,8 @@
({input = if inout then xprods @ input else input,
lexicon = if inout then Scan.extend_lexicon lexicon (SynExt.delims_of xprods) else lexicon,
gram = if inout then Parser.extend_gram gram xprods else gram,
- consts = merge_lists' consts1 consts2,
- prmodes = mode ins_string (merge_lists' prmodes1 prmodes2),
+ consts = Library.merge (op =) (consts1, consts2),
+ prmodes = insert (op =) mode (Library.merge (op =) (prmodes1, prmodes2)),
parse_ast_trtab =
extend_trtab "parse ast translation" parse_ast_translation parse_ast_trtab,
parse_ruletab = extend_ruletab parse_rules parse_ruletab,
@@ -278,11 +278,11 @@
print_ast_trtab = print_ast_trtab2, tokentrtab = tokentrtab2, prtabs = prtabs2} = tabs2;
in
Syntax
- ({input = merge_lists' input1 input2,
+ ({input = Library.merge (op =) (input1, input2),
lexicon = Scan.merge_lexicons lexicon1 lexicon2,
gram = Parser.merge_grams gram1 gram2,
consts = sort_distinct string_ord (consts1 @ consts2),
- prmodes = merge_lists prmodes1 prmodes2,
+ prmodes = Library.merge (op =) (prmodes1, prmodes2),
parse_ast_trtab =
merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
parse_ruletab = merge_ruletabs parse_ruletab1 parse_ruletab2,
--- a/src/Pure/search.ML Fri Feb 03 17:08:03 2006 +0100
+++ b/src/Pure/search.ML Fri Feb 03 23:12:28 2006 +0100
@@ -63,7 +63,7 @@
case Seq.pull q of
NONE => depth used qs
| SOME(st,stq) =>
- if satp st andalso not (gen_mem eq_thm (st, used))
+ if satp st andalso not (member eq_thm used st)
then SOME(st, Seq.make
(fn()=> depth (st::used) (stq::qs)))
else depth used (tac st :: stq :: qs)