# HG changeset patch
# User wenzelm
# Date 1684141189 -7200
# Node ID 78deba4fdf27a92314a0579c1bb06fbabab24227
# Parent  bf4d535bbfccb1bba211e10092ee7ee413e084ce
tuned: more accurate check (is_norm_hhf protect);

diff -r bf4d535bbfcc -r 78deba4fdf27 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Mon May 15 10:50:48 2023 +0200
+++ b/src/Pure/drule.ML	Mon May 15 10:59:49 2023 +0200
@@ -75,7 +75,7 @@
   val eta_contraction_rule: thm -> thm
   val norm_hhf_eq: thm
   val norm_hhf_eqs: thm list
-  val is_norm_hhf: term -> bool
+  val is_norm_hhf: {protect: bool} -> term -> bool
   val norm_hhf: theory -> term -> term
   val norm_hhf_cterm: Proof.context -> cterm -> cterm
   val protect: cterm -> cterm
@@ -669,15 +669,19 @@
 val norm_hhf_prop = Logic.dest_equals (Thm.prop_of norm_hhf_eq);
 val norm_hhf_eqs = [norm_hhf_eq, sort_constraint_eq];
 
-fun is_norm_hhf (Const ("Pure.sort_constraint", _)) = false
-  | is_norm_hhf (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false
-  | is_norm_hhf (Abs _ $ _) = false
-  | is_norm_hhf (t $ u) = is_norm_hhf t andalso is_norm_hhf u
-  | is_norm_hhf (Abs (_, _, t)) = is_norm_hhf t
-  | is_norm_hhf _ = true;
+fun is_norm_hhf {protect} =
+  let
+    fun is_norm (Const ("Pure.sort_constraint", _)) = false
+      | is_norm (Const ("Pure.imp", _) $ _ $ (Const ("Pure.all", _) $ _)) = false
+      | is_norm (Const ("Pure.prop", _) $ t) = protect orelse is_norm t
+      | is_norm (Abs _ $ _) = false
+      | is_norm (t $ u) = is_norm t andalso is_norm u
+      | is_norm (Abs (_, _, t)) = is_norm t
+      | is_norm _ = true;
+  in is_norm end;
 
 fun norm_hhf thy t =
-  if is_norm_hhf t then t
+  if is_norm_hhf {protect = false} t then t
   else Pattern.rewrite_term thy [norm_hhf_prop] [] t;
 
 fun norm_hhf_cterm ctxt raw_ct =
@@ -685,7 +689,7 @@
     val thy = Proof_Context.theory_of ctxt;
     val ct = Thm.transfer_cterm thy raw_ct;
     val t = Thm.term_of ct;
-  in if is_norm_hhf t then ct else Thm.cterm_of ctxt (norm_hhf thy t) end;
+  in if is_norm_hhf {protect = false} t then ct else Thm.cterm_of ctxt (norm_hhf thy t) end;
 
 
 (* var indexes *)
diff -r bf4d535bbfcc -r 78deba4fdf27 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon May 15 10:50:48 2023 +0200
+++ b/src/Pure/goal.ML	Mon May 15 10:59:49 2023 +0200
@@ -311,7 +311,7 @@
 fun norm_hhf_tac ctxt =
   resolve_tac ctxt [Drule.asm_rl]  (*cheap approximation -- thanks to builtin Logic.flatten_params*)
   THEN' SUBGOAL (fn (t, i) =>
-    if Drule.is_norm_hhf t then all_tac
+    if Drule.is_norm_hhf {protect = false} t then all_tac
     else rewrite_goal_tac ctxt Drule.norm_hhf_eqs i);
 
 
diff -r bf4d535bbfcc -r 78deba4fdf27 src/Pure/raw_simplifier.ML
--- 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;