--- a/src/Pure/raw_simplifier.ML Sat May 20 14:48:06 2023 +0200
+++ b/src/Pure/raw_simplifier.ML Sat May 20 16:12:37 2023 +0200
@@ -65,7 +65,6 @@
val fold_goals_tac: Proof.context -> thm list -> tactic
val norm_hhf: Proof.context -> thm -> thm
val norm_hhf_protect: Proof.context -> thm -> thm
- val norm_hhf_protect_without_context: thm -> thm
end;
signature RAW_SIMPLIFIER =
@@ -1449,9 +1448,6 @@
val norm_hhf = gen_norm_hhf {protect = false} hhf_ss;
val norm_hhf_protect = gen_norm_hhf {protect = true} hhf_protect_ss;
-fun norm_hhf_protect_without_context th =
- norm_hhf_protect (Proof_Context.init_global (Thm.theory_of_thm th)) th;
-
end;
end;