src/Pure/Isar/subgoal.ML

--- a/src/Pure/Isar/subgoal.ML	Sat Feb 17 20:03:37 2018 +0100
+++ b/src/Pure/Isar/subgoal.ML	Sun Feb 18 15:05:21 2018 +0100
@@ -44,7 +44,7 @@
 fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
   let
     val st = raw_st
-      |> Thm.transfer (Proof_Context.theory_of ctxt)
+      |> Thm.transfer' ctxt
       |> Raw_Simplifier.norm_hhf_protect ctxt;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
     val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;