src/Pure/Isar/method.ML
changeset 21579 abd2b4386a63
parent 20335 b5eca86ef9cc
child 21592 8831206d7f41
     1.1 --- a/src/Pure/Isar/method.ML	Wed Nov 29 04:11:11 2006 +0100
     1.2 +++ b/src/Pure/Isar/method.ML	Wed Nov 29 04:11:12 2006 +0100
     1.3 @@ -151,11 +151,8 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun cut_rule_tac raw_rule =
     1.8 -  let
     1.9 -    val rule = Drule.forall_intr_vars raw_rule;
    1.10 -    val revcut_rl = Drule.incr_indexes rule Drule.revcut_rl;
    1.11 -  in Tactic.rtac (rule COMP revcut_rl) end;
    1.12 +fun cut_rule_tac rule =
    1.13 +  Tactic.rtac (Drule.forall_intr_vars rule COMP_INCR revcut_rl);
    1.14  
    1.15  in
    1.16