src/HOL/Tools/reification.ML

 
 fun rewrite_with ctxt eqs = Simplifier.rewrite (put_simpset HOL_basic_ss ctxt addsimps eqs);
 
 val pure_subst = @{lemma "x == y ==> PROP P y ==> PROP P x" by simp}
 
-fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn { concl, ... } =>
-  let
-    val ct = case some_t
-     of NONE => Thm.dest_arg concl
-      | SOME t => Thm.cterm_of ctxt t
+fun lift_conv ctxt conv some_t = Subgoal.FOCUS (fn {context = ctxt', concl, ...} =>
+  let
+    val ct =
+      (case some_t of
+        NONE => Thm.dest_arg concl
+      | SOME t => Thm.cterm_of ctxt' t)
     val thm = conv ct;
   in
     if Thm.is_reflexive thm then no_tac
     else ALLGOALS (rtac (pure_subst OF [thm]))
   end) ctxt;