src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
changeset 57954 c52223cd1003
parent 57945 cacb00a569e0
child 57958 045c96e3edf0
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 14:42:35 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sat Aug 16 16:18:39 2014 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4        let
     1.5          val prop = mk_trp (mk_cont functional)
     1.6          val rules = Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems cont2cont}
     1.7 -        val tac = REPEAT_ALL_NEW (match_tac rules) 1
     1.8 +        val tac = REPEAT_ALL_NEW (match_tac (rev rules)) 1
     1.9        in
    1.10          Goal.prove_global thy [] [] prop (K tac)
    1.11        end
    1.12 @@ -189,7 +189,7 @@
    1.13    let
    1.14      val defl_simps =
    1.15        Named_Theorems.get (Proof_Context.init_global thy) @{named_theorems domain_defl_simps}
    1.16 -    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) defl_simps
    1.17 +    val rules = map (Thm.concl_of #> HOLogic.dest_Trueprop #> HOLogic.dest_eq) (rev defl_simps)
    1.18      val rules' = map (apfst mk_DEFL) tab1 @ map (apfst mk_LIFTDEFL) tab2
    1.19      fun proc1 t =
    1.20        (case dest_DEFL t of
    1.21 @@ -632,7 +632,7 @@
    1.22             simp_tac (put_simpset HOL_basic_ss ctxt addsimps tuple_rules) 1,
    1.23             simp_tac (put_simpset HOL_basic_ss ctxt addsimps map_ID_simps) 1,
    1.24             REPEAT (etac @{thm conjE} 1),
    1.25 -           REPEAT (resolve_tac (isodefl_rules @ prems) 1 ORELSE atac 1)])
    1.26 +           REPEAT (resolve_tac (rev isodefl_rules @ prems) 1 ORELSE atac 1)])
    1.27        end
    1.28      val isodefl_binds = map (Binding.prefix_name "isodefl_") dbinds
    1.29      fun conjuncts [] _ = []