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