--- a/src/Pure/raw_simplifier.ML Mon May 15 10:50:48 2023 +0200
+++ b/src/Pure/raw_simplifier.ML Mon May 15 10:59:49 2023 +0200
@@ -1423,11 +1423,11 @@
local
-fun gen_norm_hhf ss ctxt0 th0 =
+fun gen_norm_hhf protect 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
+ if Drule.is_norm_hhf protect (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;
@@ -1445,8 +1445,8 @@
in
-val norm_hhf = gen_norm_hhf hhf_ss;
-val norm_hhf_protect = gen_norm_hhf hhf_protect_ss;
+val norm_hhf = gen_norm_hhf {protect = false} hhf_ss;
+val norm_hhf_protect = gen_norm_hhf {protect = true} hhf_protect_ss;
end;