src/Pure/Isar/obtain.ML

--- a/src/Pure/Isar/obtain.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Isar/obtain.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -334,7 +334,7 @@
 
     val instT =
       fold (Term.add_tvarsT o #2) params []
-      |> map (TVar #> (fn T => apply2 (Thm.ctyp_of ctxt) (T, norm_type T)));
+      |> map (fn v => (v, Thm.ctyp_of ctxt (norm_type (TVar v))));
     val closed_rule = rule
       |> Thm.forall_intr (Thm.cterm_of ctxt (Free thesis_var))
       |> Thm.instantiate (instT, []);