# HG changeset patch
# User wenzelm
# Date 1408208491 -7200
# Node ID 045c96e3edf0fb00d0429a37b2f29224e61afa50
# Parent  e6ee35b8f4b5eefc19b3626de2c042a2ee8f84cb
clarified order of rules;

diff -r e6ee35b8f4b5 -r 045c96e3edf0 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 18:31:47 2014 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 19:01:31 2014 +0200
@@ -517,7 +517,7 @@
         val DEFL_simps =
           Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
         fun tac ctxt =
-          rewrite_goals_tac ctxt (map mk_meta_eq DEFL_simps)
+          rewrite_goals_tac ctxt (map mk_meta_eq (rev DEFL_simps))
           THEN TRY (resolve_tac defl_unfold_thms 1)
       in
         Goal.prove_global thy [] [] goal (tac o #context)
@@ -620,7 +620,7 @@
         val isodefl_rules =
           @{thms conjI isodefl_ID_DEFL isodefl_LIFTDEFL}
           @ isodefl_abs_rep_thms
-          @ Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl}
+          @ rev (Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_isodefl})
       in
         Goal.prove_global thy [] assms goal (fn {prems, context = ctxt} =>
          EVERY
@@ -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 (rev isodefl_rules @ prems) 1 ORELSE atac 1)])
+           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
       end
     val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
     fun conjuncts [] _ = []