# HG changeset patch
# User wenzelm
# Date 1408198719 -7200
# Node ID c52223cd1003b4b1c1c54b1f315adba95d97b007
# Parent  69728243a6140c28941d245fc83bc227a030f62d
clarified order of rules for match_tac/resolve_tac;

diff -r 69728243a614 -r c52223cd1003 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Sat Aug 16 14:42:35 2014 +0200
+++ b/src/HOL/HOLCF/Cfun.thy	Sat Aug 16 16:18:39 2014 +0200
@@ -148,7 +148,7 @@
       val tr = instantiate' [SOME T, SOME U] [SOME f]
           (mk_meta_eq @{thm Abs_cfun_inverse2});
       val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
-      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
+      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)));
     in SOME (perhaps (SINGLE (tac 1)) tr) end
 *}
 
diff -r 69728243a614 -r c52223cd1003 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 14:42:35 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 16:18:39 2014 +0200
@@ -151,7 +151,7 @@
       let
         val prop = mk_trp (mk_cont functional)
         val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
-        val tac = REPEAT_ALL_NEW (match_tac rules) 1
+        val tac = REPEAT_ALL_NEW (match_tac (rev rules)) 1
       in
         Goal.prove_global thy [] [] prop (K tac)
       end
@@ -189,7 +189,7 @@
   let
     val defl_simps =
       Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
-    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps
+    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) (rev defl_simps)
     val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2
     fun proc1 t =
       (case dest_DEFL t of
@@ -632,7 +632,7 @@
            simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,
            simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1,
            REPEAT (etac @{thm conjE} 1),
-           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
+           REPEAT (resolve_tac (rev isodefl_rules @ prems) 1 ORELSE atac 1)])
       end
     val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
     fun conjuncts [] _ = []
diff -r 69728243a614 -r c52223cd1003 src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Aug 16 14:42:35 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML	Sat Aug 16 16:18:39 2014 +0200
@@ -131,11 +131,11 @@
 
 val get_rec_tab = Rec_Data.get
 fun get_deflation_thms thy =
-  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation}
+  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_deflation})
 
 val map_ID_add = Named_Theorems.add @{named_theorems domain_map_ID}
 fun get_map_ID_thms thy =
-  Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID}
+  rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_map_ID})
 
 
 (******************************************************************************)
diff -r 69728243a614 -r c52223cd1003 src/HOL/HOLCF/Tools/fixrec.ML
--- a/src/HOL/HOLCF/Tools/fixrec.ML	Sat Aug 16 14:42:35 2014 +0200
+++ b/src/HOL/HOLCF/Tools/fixrec.ML	Sat Aug 16 16:18:39 2014 +0200
@@ -131,7 +131,7 @@
           "The error occurred for the goal statement:\n" ^
           Syntax.string_of_term lthy prop)
         val rules = Named_Theorems.get lthy @{named_theorems cont2cont}
-        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules))
+        val fast_tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)))
         val slow_tac = SOLVED' (simp_tac lthy)
         val tac = fast_tac 1 ORELSE slow_tac 1 ORELSE err
       in