# HG changeset patch
# User wenzelm
# Date 1684597321 -7200
# Node ID 5edd5b12017d5c5c0c6791f98afc82cf98482a61
# Parent  dd7bb7f99ad51c084a14e8d61e51af9d850e1e97
tuned signature;

diff -r dd7bb7f99ad5 -r 5edd5b12017d src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Sat May 20 17:18:44 2023 +0200
+++ b/src/Doc/Implementation/Proof.thy	Sat May 20 17:42:01 2023 +0200
@@ -270,7 +270,7 @@
   cterm list -> Proof.context -> thm list * Proof.context"} \\
   @{define_ML Assumption.add_assumes: "
   cterm list -> Proof.context -> thm list * Proof.context"} \\
-  @{define_ML Assumption.export: "bool -> Proof.context -> Proof.context -> thm -> thm"} \\
+  @{define_ML Assumption.export: "Proof.context -> Proof.context -> thm -> thm"} \\
   @{define_ML Assumption.export_term: "Proof.context -> Proof.context -> term -> term"} \\
   \end{mldecls}
 
@@ -290,9 +290,9 @@
   \<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
   \<open>#\<Longrightarrow>\<hyphen>intro\<close>, depending on goal mode.
 
-  \<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>is_goal inner outer thm\<close> exports result \<open>thm\<close>
-  from the \<open>inner\<close> context back into the \<open>outer\<close> one; \<open>is_goal = true\<close> means
-  this is a goal context. The result is in HHF normal form. Note that
+  \<^descr> \<^ML>\<open>Assumption.export\<close>~\<open>inner outer thm\<close> exports result \<open>thm\<close> from the
+  \<open>inner\<close> context back into the \<open>outer\<close> one; \<^ML>\<open>Assumption.export_goal\<close>
+  does the same in a goal context. The result is in HHF normal form. Note that
   \<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and
   \<^ML>\<open>Assumption.export\<close> in the canonical way.
 
@@ -318,7 +318,7 @@
   val eq' = Thm.symmetric eq;
 
   (*back to original context -- discharges assumption*)
-  val r = Assumption.export false ctxt1 ctxt0 eq';
+  val r = Assumption.export ctxt1 ctxt0 eq';
 \<close>
 
 text \<open>
diff -r dd7bb7f99ad5 -r 5edd5b12017d src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sat May 20 17:42:01 2023 +0200
@@ -155,7 +155,7 @@
                   if t aconv u then (asm, false)
                   else (Drule.abs_def (Variable.gen_all outer asm), true))
             end)));
-  in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export false inner outer th) end;
+  in (apply2 (map #1) (List.partition #2 defs_asms), Assumption.export inner outer th) end;
 
 (*
   [xs, xs \<equiv> as]
diff -r dd7bb7f99ad5 -r 5edd5b12017d src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/Isar/proof.ML	Sat May 20 17:42:01 2023 +0200
@@ -477,7 +477,7 @@
   in
     result
     |> map (Raw_Simplifier.norm_hhf result_ctxt #> protect_prems)
-    |> Proof_Context.goal_export result_ctxt goal_ctxt
+    |> Proof_Context.export_goal result_ctxt goal_ctxt
     |> (fn rules => Seq.lift provide_goal (EVERY (map refine rules) goal) state)
   end;
 
@@ -1096,7 +1096,7 @@
       let
         val ctxt' = context_of state';
         val export0 =
-          Assumption.export false result_ctxt (Proof_Context.augment result_text ctxt') #>
+          Assumption.export result_ctxt (Proof_Context.augment result_text ctxt') #>
           fold_rev (fn (x, v) => Thm.forall_intr_name (x, Thm.cterm_of params_ctxt v)) params #>
           Raw_Simplifier.norm_hhf_protect ctxt';
         val export = map export0 #> Variable.export result_ctxt ctxt';
diff -r dd7bb7f99ad5 -r 5edd5b12017d src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat May 20 17:42:01 2023 +0200
@@ -102,8 +102,9 @@
   val standard_typ_check: Proof.context -> typ list -> typ list
   val standard_term_check_finish: Proof.context -> term list -> term list
   val standard_term_uncheck: Proof.context -> term list -> term list
-  val goal_export: Proof.context -> Proof.context -> thm list -> thm list
+  val export_: {goal: bool} -> Proof.context -> Proof.context -> thm list -> thm list
   val export: Proof.context -> Proof.context -> thm list -> thm list
+  val export_goal: Proof.context -> Proof.context -> thm list -> thm list
   val 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
@@ -838,12 +839,12 @@
 
 (** export results **)
 
-fun common_export is_goal inner outer =
-  map (Assumption.export is_goal inner outer) #>
+fun export_ goal inner outer =
+  map (Assumption.export_ goal inner outer) #>
   Variable.export inner outer;
 
-val goal_export = common_export true;
-val export = common_export false;
+val export = export_{goal = false};
+val export_goal = export_{goal = true};
 
 fun export_morphism inner outer =
   Assumption.export_morphism inner outer $>
diff -r dd7bb7f99ad5 -r 5edd5b12017d src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/assumption.ML	Sat May 20 17:42:01 2023 +0200
@@ -18,7 +18,9 @@
   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_: {goal: bool} -> Proof.context -> Proof.context -> thm -> thm
+  val export: Proof.context -> Proof.context -> thm -> thm
+  val export_goal: Proof.context -> Proof.context -> thm -> thm
   val export_morphism: Proof.context -> Proof.context -> morphism
 end;
 
@@ -134,11 +136,14 @@
 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 =
+fun export_{goal} inner outer =
   Raw_Simplifier.norm_hhf_protect inner #>
-  export_thm is_goal inner outer #>
+  export_thm goal inner outer #>
   Raw_Simplifier.norm_hhf_protect outer;
 
+val export = export_{goal = false};
+val export_goal = export_{goal = true};
+
 fun export_morphism inner outer =
   let
     val export0 = export_thm false inner outer;
diff -r dd7bb7f99ad5 -r 5edd5b12017d src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat May 20 17:18:44 2023 +0200
+++ b/src/Pure/goal.ML	Sat May 20 17:42:01 2023 +0200
@@ -221,7 +221,7 @@
     res
     |> Thm.close_derivation \<^here>
     |> Conjunction.elim_balanced (length props)
-    |> map (Assumption.export false ctxt' ctxt)
+    |> map (Assumption.export ctxt' ctxt)
     |> Variable.export ctxt' ctxt
     |> map Drule.zero_var_indexes
   end;