--- a/src/HOL/Tools/Qelim/cooper.ML Sat Aug 16 16:18:39 2014 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Sat Aug 16 16:45:39 2014 +0200
@@ -863,7 +863,7 @@
val simpset_ctxt =
put_simpset (fst (get ctxt)) ctxt delsimps del_ths addsimps add_ths
in
- Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith})
+ Method.insert_tac (rev (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 16:18:39 2014 +0200
+++ b/src/HOL/Tools/arith_data.ML Sat Aug 16 16:45:39 2014 +0200
@@ -53,7 +53,7 @@
(Scan.succeed (fn ctxt =>
METHOD (fn facts =>
HEADGOAL
- (Method.insert_tac (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
+ (Method.insert_tac (rev (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 16:18:39 2014 +0200
+++ b/src/HOL/Tools/lin_arith.ML Sat Aug 16 16:45:39 2014 +0200
@@ -796,7 +796,7 @@
(* FIXME !?? *)
fun add_arith_facts ctxt =
- Simplifier.add_prems (Named_Theorems.get ctxt @{named_theorems arith}) ctxt;
+ Simplifier.add_prems (rev (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 (Named_Theorems.get ctxt @{named_theorems arith} @ facts)
+ HEADGOAL (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
THEN' tac ctxt)))) "linear arithmetic" #>
Arith_Data.add_tactic "linear arithmetic" gen_tac;