diff -r b4d409c65a76 -r 71467e35fc3c src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Tue Nov 26 14:32:08 2019 +0000
+++ b/src/Pure/raw_simplifier.ML	Thu Nov 28 18:13:23 2019 +0100
@@ -1426,15 +1426,14 @@
 
 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 ()