src/Pure/Isar/subgoal.ML

     val (asms, concl) =
       if do_prems then (Drule.strip_imp_prems goal, Drule.strip_imp_concl goal)
       else ([], goal);
     val text = asms @ (if do_concl then [concl] else []);
 
-    val (inst, ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
-    val schematic_terms = map (apsnd (Thm.cterm_of ctxt3)) (#2 inst);
+    val ((_, inst), ctxt3) = Variable.import_inst true (map Thm.term_of text) ctxt2;
+    val schematic_terms = Term_Subst.Vars.fold (fn (v, t) => cons (v, Thm.cterm_of ctxt3 t)) inst [];
 
     val schematics = (schematic_types, schematic_terms);
     val asms' = map (Thm.instantiate_cterm schematics) asms;
     val concl' = Thm.instantiate_cterm schematics concl;
     val (prems, context) = Assumption.add_assumes asms' ctxt3;