added apply_cond_open;

--- a/src/Pure/Isar/proof_history.ML	Wed Mar 17 13:39:21 1999 +0100
+++ b/src/Pure/Isar/proof_history.ML	Wed Mar 17 13:39:44 1999 +0100
@@ -28,6 +28,7 @@
   val apply: (Proof.state -> Proof.state) -> T -> T
   val apply_open: (Proof.state -> Proof.state) -> T -> T
   val apply_close: (Proof.state -> Proof.state) -> T -> T
+  val apply_cond_open: bool -> (Proof.state -> Proof.state) -> T -> T
 end;
 
 structure ProofHistory: PROOF_HISTORY =
@@ -105,6 +106,6 @@
 fun apply f = applys (Seq.single o f);
 fun apply_open f = applys_open (Seq.single o f);
 fun apply_close f = applys_close (Seq.single o f);
-
+fun apply_cond_open do_open f = if do_open then apply_open f else apply f;
 
 end;