slightly more abstract data handling in Fast_Lin_Arith;

--- a/src/HOL/Tools/lin_arith.ML	Thu Aug 26 17:01:12 2010 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Thu Aug 26 17:37:26 2010 +0200
@@ -769,29 +769,11 @@
 
 structure Fast_Arith = Fast_Lin_Arith(structure LA_Logic = LA_Logic and LA_Data = LA_Data);
 
-fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
-  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
-    lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
-
-fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
-  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
-    lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of};
-
-fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
-  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
-    lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
-
-fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
-  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
-    lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of};
-
-fun add_inj_thms thms = Fast_Arith.map_data (map_inj_thms (append thms));
-fun add_lessD thm = Fast_Arith.map_data (map_lessD (fn thms => thms @ [thm]));
-fun add_simps thms = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimps thms));
-fun add_simprocs procs = Fast_Arith.map_data (map_simpset (fn simpset => simpset addsimprocs procs));
-
-fun set_number_of f = Fast_Arith.map_data (map_number_of (K (serial (), f)))
-
+val add_inj_thms = Fast_Arith.add_inj_thms;
+val add_lessD = Fast_Arith.add_lessD;
+val add_simps = Fast_Arith.add_simps;
+val add_simprocs = Fast_Arith.add_simprocs;
+val set_number_of = Fast_Arith.set_number_of;
 
 fun simple_tac ctxt = Fast_Arith.lin_arith_tac ctxt false;
 val lin_arith_tac = Fast_Arith.lin_arith_tac;

--- a/src/Provers/Arith/fast_lin_arith.ML	Thu Aug 26 17:01:12 2010 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Thu Aug 26 17:37:26 2010 +0200
@@ -95,6 +95,11 @@
                      lessD: thm list, neqE: thm list, simpset: Simplifier.simpset,
                      number_of : serial * (theory -> typ -> int -> cterm)})
                 -> Context.generic -> Context.generic
+  val add_inj_thms: thm list -> Context.generic -> Context.generic
+  val add_lessD: thm -> Context.generic -> Context.generic
+  val add_simps: thm list -> Context.generic -> Context.generic
+  val add_simprocs: simproc list -> Context.generic -> Context.generic
+  val set_number_of: (theory -> typ -> int -> cterm) -> Context.generic -> Context.generic
   val trace: bool Unsynchronized.ref
 end;
 
@@ -135,13 +140,35 @@
      lessD = Thm.merge_thms (lessD1, lessD2),
      neqE = Thm.merge_thms (neqE1, neqE2),
      simpset = Simplifier.merge_ss (simpset1, simpset2),
-     (* FIXME depends on accidental load order !?! *)
+     (* FIXME depends on accidental load order !?! *)  (* FIXME *)
      number_of = if s1 > s2 then number_of1 else number_of2};
 );
 
 val map_data = Data.map;
 val get_data = Data.get o Context.Proof;
 
+fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
+  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
+    lessD = lessD, neqE = neqE, simpset = simpset, number_of = number_of};
+
+fun map_lessD f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
+  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+    lessD = f lessD, neqE = neqE, simpset = simpset, number_of = number_of};
+
+fun map_simpset f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
+  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+    lessD = lessD, neqE = neqE, simpset = f simpset, number_of = number_of};
+
+fun map_number_of f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
+  {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = inj_thms,
+    lessD = lessD, neqE = neqE, simpset = simpset, number_of = f number_of};
+
+fun add_inj_thms thms = map_data (map_inj_thms (append thms));
+fun add_lessD thm = map_data (map_lessD (fn thms => thms @ [thm]));
+fun add_simps thms = map_data (map_simpset (fn simpset => simpset addsimps thms));
+fun add_simprocs procs = map_data (map_simpset (fn simpset => simpset addsimprocs procs));
+
+fun set_number_of f = map_data (map_number_of (K (serial (), f)));
 
 
 (*** A fast decision procedure ***)