# HG changeset patch
# User wenzelm
# Date 1642852803 -3600
# Node ID 26794ec7c78e34d873c1bd17114108f02c7f2888
# Parent  e9a514c70b9add9e27c251b261aa00a302afc5a8
some updates and clarification on Assumption.export_term;

diff -r e9a514c70b9a -r 26794ec7c78e src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Fri Jan 21 23:49:10 2022 +0000
+++ b/src/Doc/Implementation/Proof.thy	Sat Jan 22 13:00:03 2022 +0100
@@ -271,11 +271,12 @@
   @{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_term: "Proof.context -> Proof.context -> term -> term"} \\
   \end{mldecls}
 
-  \<^descr> Type \<^ML_type>\<open>Assumption.export\<close> represents arbitrary export rules, which
-  is any function of type \<^ML_type>\<open>bool -> cterm list -> thm -> thm\<close>, where
-  the \<^ML_type>\<open>bool\<close> indicates goal mode, and the \<^ML_type>\<open>cterm list\<close>
+  \<^descr> Type \<^ML_type>\<open>Assumption.export\<close> represents export rules, as a pair of
+  functions \<^ML_type>\<open>bool -> cterm list -> (thm -> thm) * (term -> term)\<close>.
+  The \<^ML_type>\<open>bool\<close> argument indicates goal mode, and the \<^ML_type>\<open>cterm list\<close>
   the collection of assumptions to be discharged simultaneously.
 
   \<^descr> \<^ML>\<open>Assumption.assume\<close>~\<open>ctxt A\<close> turns proposition \<open>A\<close> into a primitive
@@ -285,13 +286,21 @@
   with export rule \<open>r\<close>. The resulting facts are hypothetical theorems as
   produced by the raw \<^ML>\<open>Assumption.assume\<close>.
 
-  \<^descr> \<^ML>\<open>Assumption.add_assumes\<close>~\<open>As\<close> is a special case of \<^ML>\<open>Assumption.add_assms\<close> where the export rule performs \<open>\<Longrightarrow>\<hyphen>intro\<close> or
+  \<^descr> \<^ML>\<open>Assumption.add_assumes\<close>~\<open>As\<close> is a special case of
+  \<^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 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
-  \<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and \<^ML>\<open>Assumption.export\<close> in the canonical way.
+  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
+  \<^ML>\<open>Proof_Context.export\<close> combines \<^ML>\<open>Variable.export\<close> and
+  \<^ML>\<open>Assumption.export\<close> in the canonical way.
+
+  \<^descr> \<^ML>\<open>Assumption.export_term\<close>~\<open>inner outer t\<close> exports term \<open>t\<close> from the
+  \<open>inner\<close> context back into the \<open>outer\<close> one. This is analogous to
+  \<^ML>\<open>Assumption.export\<close>, but only takes syntactical aspects of the
+  context into account (such as locally specified variables as seen in
+  @{command define} or @{command obtain}).
 \<close>
 
 text %mlex \<open>