# HG changeset patch
# User wenzelm
# Date 1408192346 -7200
# Node ID 1a9a6dfc255f829e924285e3b5adfe7eae791e29
# Parent  7896762b638be63489dedfba34a6705f9a4711b6
updated to named_theorems;

diff -r 7896762b638b -r 1a9a6dfc255f src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Aug 16 14:27:41 2014 +0200
+++ b/src/HOL/Nat.thy	Sat Aug 16 14:32:26 2014 +0200
@@ -12,6 +12,8 @@
 begin
 
 ML_file "~~/src/Tools/rat.ML"
+
+named_theorems arith "arith facts -- only ground formulas"
 ML_file "Tools/arith_data.ML"
 ML_file "~~/src/Provers/Arith/fast_lin_arith.ML"
 
diff -r 7896762b638b -r 1a9a6dfc255f src/HOL/Tools/Qelim/cooper.ML
--- a/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 16 14:27:41 2014 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 16 14:32:26 2014 +0200
@@ -862,9 +862,8 @@
   let
     val simpset_ctxt =
       put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths
-    val aprems = Arith_Data.get_arith_facts ctxt
   in
-    Method.insert_tac aprems
+    Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith})
     THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
     THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
     THEN_ALL_NEW simp_tac simpset_ctxt
diff -r 7896762b638b -r 1a9a6dfc255f src/HOL/Tools/arith_data.ML
--- a/src/HOL/Tools/arith_data.ML	Sat Aug 16 14:27:41 2014 +0200
+++ b/src/HOL/Tools/arith_data.ML	Sat Aug 16 14:32:26 2014 +0200
@@ -9,7 +9,6 @@
   val arith_tac: Proof.context -> int -> tactic
   val verbose_arith_tac: Proof.context -> int -> tactic
   val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
-  val get_arith_facts: Proof.context -> thm list
 
   val mk_number: typ -> int -> term
   val mk_sum: typ -> term list -> term
@@ -28,15 +27,7 @@
 structure Arith_Data: ARITH_DATA =
 struct
 
-(* slots for plugging in arithmetic facts and tactics *)
-
-structure Arith_Facts = Named_Thms
-(
-  val name = @{binding arith}
-  val description = "arith facts -- only ground formulas"
-);
-
-val get_arith_facts = Arith_Facts.get;
+(* slot for plugging in tactics *)
 
 structure Arith_Tactics = Theory_Data
 (
@@ -58,11 +49,12 @@
 val verbose_arith_tac = gen_arith_tac true;
 
 val setup =
-  Arith_Facts.setup #>
   Method.setup @{binding arith}
     (Scan.succeed (fn ctxt =>
-      METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts)
-        THEN' verbose_arith_tac ctxt))))
+      METHOD (fn facts =>
+        HEADGOAL
+        (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
+          THEN' verbose_arith_tac ctxt))))
     "various arithmetic decision procedures";
 
 
diff -r 7896762b638b -r 1a9a6dfc255f src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sat Aug 16 14:27:41 2014 +0200
+++ b/src/HOL/Tools/lin_arith.ML	Sat Aug 16 14:32:26 2014 +0200
@@ -796,7 +796,7 @@
 
 (* FIXME !?? *)
 fun add_arith_facts ctxt =
-  Simplifier.add_prems (Arith_Data.get_arith_facts ctxt) ctxt;
+  Simplifier.add_prems (Named_Theorems.get ctxt @{named_theorems arith}) ctxt;
 
 val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
 
@@ -889,7 +889,7 @@
   Method.setup @{binding linarith}
     (Scan.succeed (fn ctxt =>
       METHOD (fn facts =>
-        HEADGOAL (Method.insert_tac (Arith_Data.get_arith_facts ctxt @ facts)
+        HEADGOAL (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
           THEN' tac ctxt)))) "linear arithmetic" #>
   Arith_Data.add_tactic "linear arithmetic" gen_tac;