src/HOL/Tools/arith_data.ML
changeset 57952 1a9a6dfc255f
parent 51717 9e7d1c139569
child 57955 f28337c2c0a8
     1.1 --- a/src/HOL/Tools/arith_data.ML	Sat Aug 16 14:27:41 2014 +0200
     1.2 +++ b/src/HOL/Tools/arith_data.ML	Sat Aug 16 14:32:26 2014 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4    val arith_tac: Proof.context -> int -> tactic
     1.5    val verbose_arith_tac: Proof.context -> int -> tactic
     1.6    val add_tactic: string -> (bool -> Proof.context -> int -> tactic) -> theory -> theory
     1.7 -  val get_arith_facts: Proof.context -> thm list
     1.8  
     1.9    val mk_number: typ -> int -> term
    1.10    val mk_sum: typ -> term list -> term
    1.11 @@ -28,15 +27,7 @@
    1.12  structure Arith_Data: ARITH_DATA =
    1.13  struct
    1.14  
    1.15 -(* slots for plugging in arithmetic facts and tactics *)
    1.16 -
    1.17 -structure Arith_Facts = Named_Thms
    1.18 -(
    1.19 -  val name = @{binding arith}
    1.20 -  val description = "arith facts -- only ground formulas"
    1.21 -);
    1.22 -
    1.23 -val get_arith_facts = Arith_Facts.get;
    1.24 +(* slot for plugging in tactics *)
    1.25  
    1.26  structure Arith_Tactics = Theory_Data
    1.27  (
    1.28 @@ -58,11 +49,12 @@
    1.29  val verbose_arith_tac = gen_arith_tac true;
    1.30  
    1.31  val setup =
    1.32 -  Arith_Facts.setup #>
    1.33    Method.setup @{binding arith}
    1.34      (Scan.succeed (fn ctxt =>
    1.35 -      METHOD (fn facts => HEADGOAL (Method.insert_tac (get_arith_facts ctxt @ facts)
    1.36 -        THEN' verbose_arith_tac ctxt))))
    1.37 +      METHOD (fn facts =>
    1.38 +        HEADGOAL
    1.39 +        (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
    1.40 +          THEN' verbose_arith_tac ctxt))))
    1.41      "various arithmetic decision procedures";
    1.42  
    1.43