src/HOL/HOLCF/Cfun.thy
changeset 57954 c52223cd1003
parent 57945 cacb00a569e0
child 58880 0baae4311a9f
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Sat Aug 16 14:42:35 2014 +0200
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Sat Aug 16 16:18:39 2014 +0200
     1.3 @@ -148,7 +148,7 @@
     1.4        val tr = instantiate' [SOME T, SOME U] [SOME f]
     1.5            (mk_meta_eq @{thm Abs_cfun_inverse2});
     1.6        val rules = Named_Theorems.get ctxt @{named_theorems cont2cont};
     1.7 -      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac rules));
     1.8 +      val tac = SOLVED' (REPEAT_ALL_NEW (match_tac (rev rules)));
     1.9      in SOME (perhaps (SINGLE (tac 1)) tr) end
    1.10  *}
    1.11