diff -r a89f786b301a -r abd2b4386a63 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Nov 29 04:11:11 2006 +0100
+++ b/src/Pure/Isar/method.ML	Wed Nov 29 04:11:12 2006 +0100
@@ -151,11 +151,8 @@
 
 local
 
-fun cut_rule_tac raw_rule =
-  let
-    val rule = Drule.forall_intr_vars raw_rule;
-    val revcut_rl = Drule.incr_indexes rule Drule.revcut_rl;
-  in Tactic.rtac (rule COMP revcut_rl) end;
+fun cut_rule_tac rule =
+  Tactic.rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
 
 in