tuned;
authorwenzelm
Sun Nov 11 20:31:46 2012 +0100 (2012-11-11)
changeset 500819b92ee8dec98
parent 50080 200f749c96db
child 50082 a025340c4abb
tuned;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Sun Nov 11 16:19:55 2012 +0100
     1.2 +++ b/src/Pure/tactic.ML	Sun Nov 11 20:31:46 2012 +0100
     1.3 @@ -153,16 +153,15 @@
     1.4  val flexflex_tac = PRIMSEQ Thm.flexflex_rule;
     1.5  
     1.6  (*Remove duplicate subgoals.*)
     1.7 -val perm_tac = PRIMITIVE oo Thm.permute_prems;
     1.8 -
     1.9 +val permute_tac = PRIMITIVE oo Thm.permute_prems;
    1.10  fun distinct_tac (i, k) =
    1.11 -  perm_tac 0 (i - 1) THEN
    1.12 -  perm_tac 1 (k - 1) THEN
    1.13 +  permute_tac 0 (i - 1) THEN
    1.14 +  permute_tac 1 (k - 1) THEN
    1.15    DETERM (PRIMSEQ (fn st =>
    1.16      Thm.compose_no_flatten false (st, 0) 1
    1.17        (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
    1.18 -  perm_tac 1 (1 - k) THEN
    1.19 -  perm_tac 0 (1 - i);
    1.20 +  permute_tac 1 (1 - k) THEN
    1.21 +  permute_tac 0 (1 - i);
    1.22  
    1.23  fun distinct_subgoal_tac i st =
    1.24    (case drop (i - 1) (Thm.prems_of st) of