# HG changeset patch
# User wenzelm
# Date 1164769872 -3600
# Node ID abd2b4386a63cb1cb7ea8c80cf9d277538006590
# Parent  a89f786b301a9495ac2303e2a2ebf1b8a94bd6c1
COMP_INCR;

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
 
diff -r a89f786b301a -r abd2b4386a63 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Wed Nov 29 04:11:11 2006 +0100
+++ b/src/Pure/goal.ML	Wed Nov 29 04:11:12 2006 +0100
@@ -48,7 +48,7 @@
   --- (protect)
   #C
 *)
-fun protect th = th COMP Drule.incr_indexes th Drule.protectI;
+fun protect th = th COMP_INCR Drule.protectI;
 
 (*
   A ==> ... ==> #C