src/Provers/Arith/fast_lin_arith.ML
changeset 33519 e31a85f92ce9
parent 33317 b4534348b8fd
child 35230 be006fbcfb96
     1.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4  
     1.5  fun no_number_of _ _ _ = raise CTERM ("number_of", [])
     1.6  
     1.7 -structure Data = GenericDataFun
     1.8 +structure Data = Generic_Data
     1.9  (
    1.10    type T =
    1.11     {add_mono_thms: thm list,
    1.12 @@ -124,7 +124,7 @@
    1.13                 lessD = [], neqE = [], simpset = Simplifier.empty_ss,
    1.14                 number_of = (serial (), no_number_of) } : T;
    1.15    val extend = I;
    1.16 -  fun merge _
    1.17 +  fun merge
    1.18      ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
    1.19        lessD = lessD1, neqE=neqE1, simpset = simpset1,
    1.20        number_of = (number_of1 as (s1, _))},
    1.21 @@ -137,6 +137,7 @@
    1.22       lessD = Thm.merge_thms (lessD1, lessD2),
    1.23       neqE = Thm.merge_thms (neqE1, neqE2),
    1.24       simpset = Simplifier.merge_ss (simpset1, simpset2),
    1.25 +     (* FIXME depends on accidental load order !?! *)
    1.26       number_of = if s1 > s2 then number_of1 else number_of2};
    1.27  );
    1.28