src/HOL/Tools/lin_arith.ML
changeset 57952 1a9a6dfc255f
parent 55990 41c6b99c5fb7
child 57955 f28337c2c0a8
     1.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Aug 16 14:27:41 2014 +0200
     1.2 +++ b/src/HOL/Tools/lin_arith.ML	Sat Aug 16 14:32:26 2014 +0200
     1.3 @@ -796,7 +796,7 @@
     1.4  
     1.5  (* FIXME !?? *)
     1.6  fun add_arith_facts ctxt =
     1.7 -  Simplifier.add_prems (Arith_Data.get_arith_facts ctxt) ctxt;
     1.8 +  Simplifier.add_prems (Named_Theorems.get ctxt @{named_theorems arith}) ctxt;
     1.9  
    1.10  val simproc = add_arith_facts #> Fast_Arith.lin_arith_simproc;
    1.11  
    1.12 @@ -889,7 +889,7 @@
    1.13    Method.setup @{binding linarith}
    1.14      (Scan.succeed (fn ctxt =>
    1.15        METHOD (fn facts =>
    1.16 -        HEADGOAL (Method.insert_tac (Arith_Data.get_arith_facts ctxt @ facts)
    1.17 +        HEADGOAL (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
    1.18            THEN' tac ctxt)))) "linear arithmetic" #>
    1.19    Arith_Data.add_tactic "linear arithmetic" gen_tac;
    1.20