--- 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"
--- 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
--- 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";
--- 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;