# HG changeset patch
# User wenzelm
# Date 1408200339 -7200
# Node ID f28337c2c0a85c158f485d14c164f9e30f3e91ed
# Parent  c52223cd1003b4b1c1c54b1f315adba95d97b007
clarified order of arith rules;

diff -r c52223cd1003 -r f28337c2c0a8 src/HOL/Tools/Qelim/cooper.ML
--- 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
diff -r c52223cd1003 -r f28337c2c0a8 src/HOL/Tools/arith_data.ML
--- 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";
 
diff -r c52223cd1003 -r f28337c2c0a8 src/HOL/Tools/lin_arith.ML
--- 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;