src/Pure/Isar/isar_thy.ML

--- a/src/Pure/Isar/isar_thy.ML	Fri Jan 28 21:55:43 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Fri Jan 28 21:56:02 2000 +0100
@@ -116,6 +116,8 @@
   val begin_block: ProofHistory.T -> ProofHistory.T
   val next_block: ProofHistory.T -> ProofHistory.T
   val end_block: ProofHistory.T -> ProofHistory.T
+  val defer: int option -> ProofHistory.T -> ProofHistory.T
+  val prefer: int -> ProofHistory.T -> ProofHistory.T
   val tac: Method.text -> ProofHistory.T -> ProofHistory.T
   val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
   val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
@@ -342,6 +344,12 @@
 val end_block = ProofHistory.applys Proof.end_block;
 
 
+(* shuffle state *)
+
+fun defer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.defer i))));
+fun prefer i = ProofHistory.applys (Method.refine (Method.Basic (K (Method.prefer i))));
+
+
 (* backward steps *)
 
 val tac = ProofHistory.applys o Method.refine_no_facts;