--- a/doc-src/IsarRef/pure.tex Wed May 17 18:27:13 2000 +0200
+++ b/doc-src/IsarRef/pure.tex Thu May 18 11:40:57 2000 +0200
@@ -1017,9 +1017,10 @@
order to complete the proof properly, any of the actual structured proof
commands (e.g.\ ``$\DOT$'') has to be given eventually.
- Facts are passed to $m$ as indicated by the goal's forward-chain mode.
- Common use of $\isarkeyword{apply}$ would be in a purely backward manner,
- though.
+ Facts are passed to $m$ as indicated by the goal's forward-chain mode, and
+ are \emph{consumed} afterwards. Thus any further $\isarkeyword{apply}$
+ command would always work in a purely backward manner.
+
\item [$\isarkeyword{apply_end}~(m)$] applies proof method $m$ as if in
terminal position. Basically, this simulates a multi-step tactic script for
$\QEDNAME$, but may be given anywhere within the proof body.
--- a/src/Pure/Isar/isar_thy.ML Wed May 17 18:27:13 2000 +0200
+++ b/src/Pure/Isar/isar_thy.ML Thu May 18 11:40:57 2000 +0200
@@ -379,9 +379,11 @@
(* backward steps *)
-fun apply (m, comment_ignore) = ProofHistory.applys (Method.refine m o Proof.assert_backward);
-fun apply_end (m, comment_ignore) =
- ProofHistory.applys (Method.refine_end m o Proof.assert_forward);
+fun apply (m, comment_ignore) = ProofHistory.applys
+ (Seq.map (Proof.goal_facts (K [])) o Method.refine m o Proof.assert_backward);
+
+fun apply_end (m, comment_ignore) = ProofHistory.applys
+ (Method.refine_end m o Proof.assert_forward);
val proof = ProofHistory.applys o Method.proof o
apsome Comment.ignore_interest o Comment.ignore_interest' o Comment.ignore;