# HG changeset patch
# User wenzelm
# Date 958642857 -7200
# Node ID 0467dd0d66ff2aff496f98f0f01a9a0f5169bc9b
# Parent  3a5215883047a1d378dc1f0246f79f2a08cdf948
'apply' consumes facts;

diff -r 3a5215883047 -r 0467dd0d66ff doc-src/IsarRef/pure.tex
--- 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.
diff -r 3a5215883047 -r 0467dd0d66ff src/Pure/Isar/isar_thy.ML
--- 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;