# HG changeset patch
# User wenzelm
# Date 949093015 -3600
# Node ID 7574835ed01e8f5406ca7571f16ddd6377911596
# Parent  97414b447a022501a0de07a28497d3f0bd3cf0d7
added prefer, defer;

diff -r 97414b447a02 -r 7574835ed01e src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Jan 28 21:56:37 2000 +0100
+++ b/src/Pure/Isar/method.ML	Fri Jan 28 21:56:55 2000 +0100
@@ -28,6 +28,8 @@
   val METHOD0: tactic -> Proof.method
   val fail: Proof.method
   val succeed: Proof.method
+  val defer: int option -> Proof.method
+  val prefer: int -> Proof.method
   val insert_tac: thm list -> int -> tactic
   val insert: thm list -> Proof.method
   val insert_facts: Proof.method
@@ -195,6 +197,12 @@
 val succeed = METHOD (K all_tac);
 
 
+(* shuffle *)
+
+fun prefer i = METHOD (K (PRIMITIVE (Thm.permute_prems 0 (i - 1))));
+fun defer opt_i = METHOD (K (Tactic.defer_tac (if_none opt_i 1)));
+
+
 (* insert *)
 
 local