# HG changeset patch # User wenzelm # Date 1139004748 -3600 # Node ID f47c46d7d654f6b7a140a2adcebf64427c3e2971 # Parent 7635e0060cd4199891eaff15aa5bd1af00a7f020 canonical member/insert/merge; diff -r 7635e0060cd4 -r f47c46d7d654 src/HOL/Import/hol4rews.ML --- 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) diff -r 7635e0060cd4 -r f47c46d7d654 src/HOL/Tools/inductive_package.ML --- 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); diff -r 7635e0060cd4 -r f47c46d7d654 src/HOL/Tools/specification_package.ML --- 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... *) diff -r 7635e0060cd4 -r f47c46d7d654 src/Pure/General/graph.ML --- 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 diff -r 7635e0060cd4 -r f47c46d7d654 src/Pure/Isar/context_rules.ML --- 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) diff -r 7635e0060cd4 -r f47c46d7d654 src/Pure/Isar/method.ML --- 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); diff -r 7635e0060cd4 -r f47c46d7d654 src/Pure/Isar/net_rules.ML --- 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}) = diff -r 7635e0060cd4 -r f47c46d7d654 src/Pure/Proof/extraction.ML --- 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, diff -r 7635e0060cd4 -r f47c46d7d654 src/Pure/Syntax/syntax.ML --- 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, diff -r 7635e0060cd4 -r f47c46d7d654 src/Pure/search.ML --- 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)