src/Pure/raw_simplifier.ML

 
 (* HHF normal form: \<And> before \<Longrightarrow>, outermost \<And> generalized *)
 
 local
 
-fun gen_norm_hhf ss ctxt =
-  Thm.transfer' ctxt #>
-  (fn th =>
-    if Drule.is_norm_hhf (Thm.prop_of th) then th
-    else
-      Conv.fconv_rule
-        (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th) #>
-  Thm.adjust_maxidx_thm ~1 #>
-  Variable.gen_all ctxt;
+fun gen_norm_hhf ss ctxt0 th0 =
+  let
+    val (ctxt, th) = Thm.join_transfer_context (ctxt0, th0);
+    val th' =
+      if Drule.is_norm_hhf (Thm.prop_of th) then th
+      else
+        Conv.fconv_rule (rewrite_cterm (true, false, false) (K (K NONE)) (put_simpset ss ctxt)) th;
+  in th' |> Thm.adjust_maxidx_thm ~1 |> Variable.gen_all ctxt end;
 
 val hhf_ss =
   Context.the_local_context ()
   |> init_simpset Drule.norm_hhf_eqs
   |> simpset_of;