src/Pure/subgoal.ML

--- a/src/Pure/subgoal.ML	Wed Mar 04 20:50:20 2015 +0100
+++ b/src/Pure/subgoal.ML	Wed Mar 04 22:05:01 2015 +0100
@@ -70,7 +70,7 @@
     val cert = Proof_Context.cterm_of ctxt;
     val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
 
-    val Ts = map (#T o Thm.rep_cterm) params;
+    val Ts = map Thm.typ_of_cterm params;
     val ts = map Thm.term_of params;
 
     val prop = Thm.full_prop_of th';