COMP_INCR;
authorwenzelm
Wed Nov 29 04:11:12 2006 +0100 (2006-11-29)
changeset 21579abd2b4386a63
parent 21578 a89f786b301a
child 21580 ff8062cd41e9
COMP_INCR;
src/Pure/Isar/method.ML
src/Pure/goal.ML
     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  
     2.1 --- a/src/Pure/goal.ML	Wed Nov 29 04:11:11 2006 +0100
     2.2 +++ b/src/Pure/goal.ML	Wed Nov 29 04:11:12 2006 +0100
     2.3 @@ -48,7 +48,7 @@
     2.4    --- (protect)
     2.5    #C
     2.6  *)
     2.7 -fun protect th = th COMP Drule.incr_indexes th Drule.protectI;
     2.8 +fun protect th = th COMP_INCR Drule.protectI;
     2.9  
    2.10  (*
    2.11    A ==> ... ==> #C