--- a/src/Pure/goal.ML Sat May 20 14:48:06 2023 +0200
+++ b/src/Pure/goal.ML Sat May 20 16:12:37 2023 +0200
@@ -22,7 +22,6 @@
val check_finished: Proof.context -> thm -> thm
val finish: Proof.context -> thm -> thm
val norm_result: Proof.context -> thm -> thm
- val norm_result_without_context: thm -> thm
val skip_proofs_enabled: unit -> bool
val future_result: Proof.context -> thm future -> term -> thm
val prove_internal: Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm
@@ -97,9 +96,6 @@
#> Thm.strip_shyps
#> Drule.zero_var_indexes;
-fun norm_result_without_context th =
- norm_result (Proof_Context.init_global (Thm.theory_of_thm th)) th;
-
(* scheduling parameters *)