src/HOL/HOLCF/Cfun.thy

--- a/src/HOL/HOLCF/Cfun.thy	Wed Mar 04 20:50:20 2015 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Wed Mar 04 22:05:01 2015 +0100
@@ -144,7 +144,7 @@
     let
       val dest = Thm.dest_comb;
       val f = (snd o dest o snd o dest) ct;
-      val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_term f);
+      val [T, U] = Thm.dest_ctyp (Thm.ctyp_of_cterm f);
       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};