# HG changeset patch
# User wenzelm
# Date 1684591957 -7200
# Node ID f0aca0506531c586c935dcd86e482bb016b13c69
# Parent  3357bc875b11f7957829964885455d49098570de
more robust context: fail immediately via Morphism.the_theory, instead of rarely via Thm.theory_of_thm (for non-normal thm);

diff -r 3357bc875b11 -r f0aca0506531 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat May 20 14:48:06 2023 +0200
+++ b/src/Pure/Isar/local_theory.ML	Sat May 20 16:12:37 2023 +0200
@@ -195,7 +195,8 @@
 
 fun standard_morphism lthy ctxt =
   Morphism.set_context' lthy
-   (Proof_Context.norm_export_morphism lthy ctxt $>
+   (Proof_Context.export_morphism lthy ctxt $>
+    Morphism.thm_morphism' "Local_Theory.standard" (Goal.norm_result o Proof_Context.init_global) $>
     Morphism.binding_morphism "Local_Theory.standard_binding"
       (Name_Space.transform_binding (Proof_Context.naming_of lthy)));
 
diff -r 3357bc875b11 -r f0aca0506531 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat May 20 14:48:06 2023 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat May 20 16:12:37 2023 +0200
@@ -105,7 +105,6 @@
   val goal_export: Proof.context -> Proof.context -> thm list -> thm list
   val export: Proof.context -> Proof.context -> thm list -> thm list
   val export_morphism: Proof.context -> Proof.context -> morphism
-  val norm_export_morphism: Proof.context -> Proof.context -> morphism
   val auto_bind_goal: term list -> Proof.context -> Proof.context
   val auto_bind_facts: term list -> Proof.context -> Proof.context
   val simult_matches: Proof.context -> term * term list -> (indexname * term) list
@@ -850,10 +849,6 @@
   Assumption.export_morphism inner outer $>
   Variable.export_morphism inner outer;
 
-fun norm_export_morphism inner outer =
-  export_morphism inner outer $>
-  Morphism.thm_morphism "Proof_Context.norm_export" Goal.norm_result_without_context;
-
 
 
 (** term bindings **)
diff -r 3357bc875b11 -r f0aca0506531 src/Pure/Isar/token.ML
--- a/src/Pure/Isar/token.ML	Sat May 20 14:48:06 2023 +0200
+++ b/src/Pure/Isar/token.ML	Sat May 20 16:12:37 2023 +0200
@@ -785,8 +785,9 @@
 
 (* wrapped syntax *)
 
-fun syntax_generic scan src context =
+fun syntax_generic scan src0 context =
   let
+    val src = map (transfer (Context.theory_of context)) src0;
     val (name, pos) = name_of_src src;
     val old_reports = maps reports_of_value src;
     val args1 = map init_assignable (args_of_src src);
diff -r 3357bc875b11 -r f0aca0506531 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Sat May 20 14:48:06 2023 +0200
+++ b/src/Pure/assumption.ML	Sat May 20 16:12:37 2023 +0200
@@ -17,8 +17,8 @@
   val local_prems_of: Proof.context -> Proof.context -> thm list
   val add_assms: export -> cterm list -> Proof.context -> thm list * Proof.context
   val add_assumes: cterm list -> Proof.context -> thm list * Proof.context
+  val export_term: Proof.context -> Proof.context -> term -> term
   val export: bool -> Proof.context -> Proof.context -> thm -> thm
-  val export_term: Proof.context -> Proof.context -> term -> term
   val export_morphism: Proof.context -> Proof.context -> morphism
 end;
 
@@ -128,22 +128,29 @@
 
 (* export *)
 
-fun export is_goal inner outer =
-  Raw_Simplifier.norm_hhf_protect_without_context #>
-  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer) #>
-  Raw_Simplifier.norm_hhf_protect_without_context;
-
 fun export_term inner outer =
   fold_rev (fn (e, As) => #2 (e false As)) (local_assumptions_of inner outer);
 
+fun export_thm is_goal inner outer =
+  fold_rev (fn (e, As) => #1 (e is_goal As)) (local_assumptions_of inner outer);
+
+fun export is_goal inner outer =
+  Raw_Simplifier.norm_hhf_protect inner #>
+  export_thm is_goal inner outer #>
+  Raw_Simplifier.norm_hhf_protect outer;
+
 fun export_morphism inner outer =
   let
-    val thm = export false inner outer;
+    val export0 = export_thm false inner outer;
+    fun thm thy =
+      let val norm = norm_hhf_protect (Proof_Context.init_global thy)
+      in norm #> export0 #> norm end;
     val term = export_term inner outer;
     val typ = Logic.type_map term;
   in
     Morphism.morphism "Assumption.export"
-      {binding = [], typ = [K typ], term = [K term], fact = [K (map thm)]}
+      {binding = [], typ = [K typ], term = [K term], fact = [map o thm o Morphism.the_theory]}
+    |> Morphism.set_context (Proof_Context.theory_of inner)
   end;
 
 end;
diff -r 3357bc875b11 -r f0aca0506531 src/Pure/goal.ML
--- 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 *)
 
diff -r 3357bc875b11 -r f0aca0506531 src/Pure/raw_simplifier.ML
--- 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;