# HG changeset patch
# User wenzelm
# Date 1684152585 -7200
# Node ID ec817f4486b3e1205dee137b61e097c079b697a8
# Parent  c8c084bd7e1275bd5ee41c8c0373942dc7112376
more operations "without_context", assuming that the thm has been properly transferred already;

diff -r c8c084bd7e12 -r ec817f4486b3 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon May 15 12:14:47 2023 +0200
+++ b/src/Pure/goal.ML	Mon May 15 14:09:45 2023 +0200
@@ -22,6 +22,7 @@
   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
@@ -96,6 +97,9 @@
   #> 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 *)
 
diff -r c8c084bd7e12 -r ec817f4486b3 src/Pure/raw_simplifier.ML
--- a/src/Pure/raw_simplifier.ML	Mon May 15 12:14:47 2023 +0200
+++ b/src/Pure/raw_simplifier.ML	Mon May 15 14:09:45 2023 +0200
@@ -65,6 +65,7 @@
   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 =
@@ -1448,6 +1449,9 @@
 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;