--- a/src/Pure/Isar/method.ML Tue Oct 16 16:50:03 2012 +0200
+++ b/src/Pure/Isar/method.ML Tue Oct 16 17:47:23 2012 +0200
@@ -20,8 +20,6 @@
val SIMPLE_METHOD: tactic -> method
val SIMPLE_METHOD': (int -> tactic) -> method
val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
- val defer: int option -> method
- val prefer: int -> method
val cheating: bool -> Proof.context -> method
val intro: thm list -> method
val elim: thm list -> method
@@ -124,12 +122,6 @@
end;
-(* shuffle subgoals *)
-
-fun prefer i = METHOD (K (Tactic.defer_tac i THEN PRIMITIVE (Thm.permute_prems 0 ~1)));
-fun defer opt_i = METHOD (K (Tactic.defer_tac (the_default 1 opt_i)));
-
-
(* cheating *)
fun cheating int ctxt =