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
 *}