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>