# HG changeset patch # User haftmann # Date 1176272895 -7200 # Node ID 399e4b4835dadc35c2780d95235102bbb3ffc918 # Parent a47e4fd7ebc194b2666370c990b8d921adbed297 canonical merge operations diff -r a47e4fd7ebc1 -r 399e4b4835da src/HOL/Algebra/ringsimp.ML --- a/src/HOL/Algebra/ringsimp.ML Wed Apr 11 08:28:14 2007 +0200 +++ b/src/HOL/Algebra/ringsimp.ML Wed Apr 11 08:28:15 2007 +0200 @@ -29,8 +29,7 @@ identifier and operations identify the structure uniquely. *) val empty = []; val extend = I; - fun merge _ (structs1, structs2) = gen_merge_lists - (fn ((s1, _), (s2, _)) => struct_eq (s1, s2)) structs1 structs2; + fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop)); fun print generic structs = let val ctxt = Context.proof_of generic; @@ -64,14 +63,11 @@ (** Attribute **) fun add_struct_thm s = - Thm.declaration_attribute (fn thm => fn ctxt => - AlgebraData.map (fn structs => - if AList.defined struct_eq structs s - then AList.map_entry struct_eq s (fn thms => thm :: thms) structs - else (s, [thm])::structs) ctxt); + Thm.declaration_attribute + (fn thm => AlgebraData.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm))); fun del_struct s = - Thm.declaration_attribute (fn _ => fn ctxt => - AlgebraData.map (AList.delete struct_eq s) ctxt); + Thm.declaration_attribute + (fn _ => AlgebraData.map (AList.delete struct_eq s)); val attribute = Attrib.syntax (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon || diff -r a47e4fd7ebc1 -r 399e4b4835da src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Wed Apr 11 08:28:14 2007 +0200 +++ b/src/HOL/Tools/record_package.ML Wed Apr 11 08:28:15 2007 +0200 @@ -299,9 +299,9 @@ {selectors = Symtab.merge (K true) (sels1, sels2), updates = Symtab.merge (K true) (upds1, upds2), simpset = Simplifier.merge_ss (ss1, ss2)} - (Symtab.merge Thm.eq_thm (equalities1, equalities2)) - (gen_merge_lists Thm.eq_thm extinjects1 extinjects2) - (Symtab.merge Thm.eq_thm (extsplit1,extsplit2)) + (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2)) + (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2)) + (Symtab.merge Thm.eq_thm_prop (extsplit1,extsplit2)) (Symtab.merge (fn ((a,b,c,d),(w,x,y,z)) => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z)) @@ -384,11 +384,11 @@ let val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} = RecordsData.get thy; - val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit + val data = make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit splits extfields fieldext; in RecordsData.put data thy end; -fun get_extinjects thy = #extinjects (RecordsData.get thy); +val get_extinjects = rev o #extinjects o RecordsData.get; (* access 'extsplit' *) diff -r a47e4fd7ebc1 -r 399e4b4835da src/HOL/arith_data.ML --- a/src/HOL/arith_data.ML Wed Apr 11 08:28:14 2007 +0200 +++ b/src/HOL/arith_data.ML Wed Apr 11 08:28:15 2007 +0200 @@ -209,8 +209,6 @@ fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2); -val merge_arith_tactics = gen_merge_lists eq_arith_tactic; - structure ArithTheoryData = TheoryDataFun (struct val name = "HOL/arith"; @@ -223,25 +221,25 @@ val extend = I; fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1}, {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) = - {splits = Drule.merge_rules (splits1, splits2), - inj_consts = merge_lists inj_consts1 inj_consts2, - discrete = merge_lists discrete1 discrete2, - tactics = merge_arith_tactics tactics1 tactics2}; + {splits = Library.merge Thm.eq_thm_prop (splits1, splits2), + inj_consts = Library.merge (op =) (inj_consts1, inj_consts2), + discrete = Library.merge (op =) (discrete1, discrete2), + tactics = Library.merge eq_arith_tactic (tactics1, tactics2)}; fun print _ _ = (); end); val arith_split_add = Thm.declaration_attribute (fn thm => Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => - {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})) I); + {splits= insert Thm.eq_thm_prop thm splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})) I); fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => - {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, tactics= tactics}); + {splits = splits, inj_consts = inj_consts, discrete = insert (op =) d discrete, tactics= tactics}); fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => - {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, tactics= tactics}); + {splits = splits, inj_consts = insert (op =) c inj_consts, discrete = discrete, tactics= tactics}); fun arith_tactic_add tac = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} => - {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= merge_arith_tactics tactics [tac]}); + {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= insert eq_arith_tactic tac tactics}); signature HOL_LIN_ARITH_DATA =