# HG changeset patch
# User wenzelm
# Date 921674384 -3600
# Node ID a67e4729efb2495a0ec77812345218815d82bc19
# Parent  47b357194f328ffbfc0926844187b0bc0ad4f1d2
added apply_cond_open;

diff -r 47b357194f32 -r a67e4729efb2 src/Pure/Isar/proof_history.ML
--- 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;