added prefer, defer;

--- 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