# HG changeset patch
# User nipkow
# Date 1234214137 -3600
# Node ID 55ddff2ed906ecc56a0ed41d586eb2049a1a5e3d
# Parent  a7c164e228e1d808bbbeb8ac86e99e2c3e3f5dc2# Parent  14d9891c917b15bbd025f4d40d6d7443bfa3a7e6
merged

diff -r a7c164e228e1 -r 55ddff2ed906 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Feb 09 17:25:07 2009 +1100
+++ b/src/HOL/Nat.thy	Mon Feb 09 22:15:37 2009 +0100
@@ -1336,12 +1336,19 @@
 use "Tools/arith_data.ML"
 declaration {* K ArithData.setup *}
 
+ML{*
+structure ArithFacts =
+  NamedThmsFun(val name = "arith"
+               val description = "arith facts - only ground formulas");
+*}
+
+setup ArithFacts.setup
+
 use "Tools/lin_arith.ML"
 declaration {* K LinArith.setup *}
 
 lemmas [arith_split] = nat_diff_split split_min split_max
 
-
 context order
 begin
 
diff -r a7c164e228e1 -r 55ddff2ed906 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Feb 09 17:25:07 2009 +1100
+++ b/src/HOL/Tools/lin_arith.ML	Mon Feb 09 22:15:37 2009 +0100
@@ -814,11 +814,14 @@
       addsimprocs ArithData.nat_cancel_sums_add}) #>
   arith_discrete "nat";
 
-val lin_arith_simproc = Fast_Arith.lin_arith_simproc;
+fun add_arith_facts ss =
+  add_prems (ArithFacts.get (MetaSimplifier.the_context ss)) ss;
+
+val lin_arith_simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
 
 val fast_nat_arith_simproc =
   Simplifier.simproc (the_context ()) "fast_nat_arith"
-    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K Fast_Arith.lin_arith_simproc);
+    ["(m::nat) < n","(m::nat) <= n", "(m::nat) = n"] (K lin_arith_simproc);
 
 (* Because of fast_nat_arith_simproc, the arithmetic solver is really only
 useful to detect inconsistencies among the premises for subgoals which are
@@ -912,7 +915,8 @@
 fun arith_method src =
   Method.syntax Args.bang_facts src
   #> (fn (prems, ctxt) => Method.METHOD (fn facts =>
-      HEADGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac ctxt)));
+      HEADGOAL (Method.insert_tac (prems @ ArithFacts.get ctxt @ facts)
+      THEN' arith_tac ctxt)));
 
 end;
 
@@ -922,7 +926,8 @@
 val setup =
   init_arith_data #>
   Simplifier.map_ss (fn ss => ss addsimprocs [fast_nat_arith_simproc]
-    addSolver (mk_solver' "lin_arith" Fast_Arith.cut_lin_arith_tac)) #>
+    addSolver (mk_solver' "lin_arith"
+      (add_arith_facts #> Fast_Arith.cut_lin_arith_tac))) #>
   Context.mapping
    (setup_options #>
     Method.add_methods