src/HOL/Tools/Qelim/cooper.ML
changeset 57952 1a9a6dfc255f
parent 57514 bdc2c6b40bf2
child 57955 f28337c2c0a8
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 16 14:27:41 2014 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Sat Aug 16 14:32:26 2014 +0200
     1.3 @@ -862,9 +862,8 @@
     1.4    let
     1.5      val simpset_ctxt =
     1.6        put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths
     1.7 -    val aprems = Arith_Data.get_arith_facts ctxt
     1.8    in
     1.9 -    Method.insert_tac aprems
    1.10 +    Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith})
    1.11      THEN_ALL_NEW Object_Logic.full_atomize_tac ctxt
    1.12      THEN_ALL_NEW CONVERSION Thm.eta_long_conversion
    1.13      THEN_ALL_NEW simp_tac simpset_ctxt