src/Pure/drule.ML

--- a/src/Pure/drule.ML	Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Pure/drule.ML	Wed Mar 04 22:05:01 2015 +0100
@@ -649,7 +649,7 @@
     val thy = Thm.theory_of_cterm ct;
     val cert = Thm.cterm_of thy;
     val certT = Thm.ctyp_of thy;
-    val T = Thm.typ_of (Thm.ctyp_of_term ct);
+    val T = Thm.typ_of_cterm ct;
     val a = certT (TVar (("'a", 0), []));
     val x = cert (Var (("x", 0), T));
   in Thm.instantiate ([(a, certT T)], [(x, ct)]) termI end;