1.1 --- a/src/HOL/Tools/lin_arith.ML	Thu Aug 26 17:01:12 2010 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 26 17:37:26 2010 +0200
     1.3 @@ -769,29 +769,11 @@
     1.4  
     1.5  structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
     1.6  
     1.7 -fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
     1.8 -  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
     1.9 -    lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
    1.10 -
    1.11 -fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    1.12 -  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    1.13 -    lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of};
    1.14 -
    1.15 -fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    1.16 -  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    1.17 -    lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
    1.18 -
    1.19 -fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    1.20 -  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    1.21 -    lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of};
    1.22 -
    1.23 -fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
    1.24 -fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
    1.25 -fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
    1.26 -fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
    1.27 -
    1.28 -fun set_number_of f = Fast_Arith.map_data (map_number_of (K (serial (), f)))
    1.29 -
    1.30 +val add_inj_thms = Fast_Arith.add_inj_thms;
    1.31 +val add_lessD = Fast_Arith.add_lessD;
    1.32 +val add_simps = Fast_Arith.add_simps;
    1.33 +val add_simprocs = Fast_Arith.add_simprocs;
    1.34 +val set_number_of = Fast_Arith.set_number_of;
    1.35  
    1.36  fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
    1.37  val lin_arith_tac = Fast_Arith.lin_arith_tac;

     2.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Thu Aug 26 17:01:12 2010 +0200
     2.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Aug 26 17:37:26 2010 +0200
     2.3 @@ -95,6 +95,11 @@
     2.4                       lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
     2.5                       number_of : serial * (theory -> typ -> int -> cterm)})
     2.6                  -> Context.generic -> Context.generic
     2.7 +  val add_inj_thms: thm list -> Context.generic -> Context.generic
     2.8 +  val add_lessD: thm -> Context.generic -> Context.generic
     2.9 +  val add_simps: thm list -> Context.generic -> Context.generic
    2.10 +  val add_simprocs: simproc list -> Context.generic -> Context.generic
    2.11 +  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
    2.12    val trace: bool Unsynchronized.ref
    2.13  end;
    2.14  
    2.15 @@ -135,13 +140,35 @@
    2.16       lessD = Thm.merge_thms (lessD1, lessD2),
    2.17       neqE = Thm.merge_thms (neqE1, neqE2),
    2.18       simpset = Simplifier.merge_ss (simpset1, simpset2),
    2.19 -     (* FIXME depends on accidental load order !?! *)
    2.20 +     (* FIXME depends on accidental load order !?! *)  (* FIXME *)
    2.21       number_of = if s1 > s2 then number_of1 else number_of2};
    2.22  );
    2.23  
    2.24  val map_data = Data.map;
    2.25  val get_data = Data.get o Context.Proof;
    2.26  
    2.27 +fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.28 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
    2.29 +    lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
    2.30 +
    2.31 +fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.32 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    2.33 +    lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of};
    2.34 +
    2.35 +fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.36 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    2.37 +    lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
    2.38 +
    2.39 +fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    2.40 +  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
    2.41 +    lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of};
    2.42 +
    2.43 +fun add_inj_thms thms = map_data (map_inj_thms (append thms));
    2.44 +fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [thm]));
    2.45 +fun add_simps thms = map_data (map_simpset (fn simpset => simpset addsimps thms));
    2.46 +fun add_simprocs procs = map_data (map_simpset (fn simpset => simpset addsimprocs procs));
    2.47 +
    2.48 +fun set_number_of f = map_data (map_number_of (K (serial (), f)));
    2.49  
    2.50  
    2.51  (*** A fast decision procedure ***)