--- 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 ()