diff -r f6e8293747fd -r 48dd1cefb4ae src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/Pure/Isar/generic_target.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -271,12 +271,13 @@
       |>> map Logic.dest_type;
 
     val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
-    val inst = filter (is_Var o fst) (vars ~~ frees);
-    val cinstT = instT
-      |> map (apply2 (Thm.ctyp_of ctxt) o apfst TVar);
-    val cinst = inst
-      |> map (apply2 (Thm.cterm_of ctxt o Term.map_types (Term_Subst.instantiateT instT)));
-    val result' = Thm.instantiate (cinstT, cinst) result;
+    val inst =
+      map_filter
+        (fn (Var (xi, T), t) =>
+          SOME ((xi, Term_Subst.instantiateT instT T),
+            Thm.cterm_of ctxt (Term.map_types (Term_Subst.instantiateT instT) t))
+        | _ => NONE) (vars ~~ frees);
+    val result' = Thm.instantiate (map (apsnd (Thm.ctyp_of ctxt)) instT, inst) result;
 
     (*import assumes/defines*)
     val result'' =