# HG changeset patch # User haftmann # Date 1273157848 -7200 # Node ID b6a47c7d6125476d43e6e63c358b080e3e85f4c8 # Parent 4a7709f041a89a86a0a472b10983b1a3bbfd04d2 more canonical data administration diff -r 4a7709f041a8 -r b6a47c7d6125 src/HOL/Tools/Groebner_Basis/normalizer.ML --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 16:53:35 2010 +0200 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 16:57:28 2010 +0200 @@ -50,15 +50,12 @@ mk_const: ctyp -> Rat.rat -> cterm, conv: Proof.context -> cterm -> thm}; -val eq_key = Thm.eq_thm; -fun eq_data arg = eq_fst eq_key arg; - structure Data = Generic_Data ( type T = (thm * entry) list; val empty = []; val extend = I; - val merge = AList.merge eq_key (K true); + val merge = AList.merge Thm.eq_thm (K true); ); val get = Data.get o Context.Proof; @@ -109,9 +106,7 @@ fun undefined _ = raise Match; -fun del_data key = remove eq_data (key, []); - -val del = Thm.declaration_attribute (Data.map o del_data); +val del = Thm.declaration_attribute (Data.map o AList.delete Thm.eq_thm); fun add {semiring = (sr_ops, sr_rules), ring = (r_ops, r_rules), field = (f_ops, f_rules), idom, ideal} = @@ -157,7 +152,7 @@ val field = (f_ops, f_rules'); val ideal' = map (symmetric o mk_meta) ideal in - del_data key #> + AList.delete Thm.eq_thm key #> cons (key, ({vars = vars, semiring = semiring, ring = ring, field = field, idom = idom, ideal = ideal'}, {is_const = undefined, dest_const = undefined, mk_const = undefined, @@ -171,11 +166,11 @@ Data.map (fn data => let val key = Morphism.thm phi raw_key; - val _ = AList.defined eq_key data key orelse + val _ = AList.defined Thm.eq_thm data key orelse raise THM ("No data entry for structure key", 0, [key]); val fns = {is_const = is_const phi, dest_const = dest_const phi, mk_const = mk_const phi, conv = conv phi}; - in AList.map_entry eq_key key (apsnd (K fns)) data end); + in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end); (* concrete syntax *)