diff -r 200f749c96db -r 9b92ee8dec98 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Sun Nov 11 16:19:55 2012 +0100
+++ b/src/Pure/tactic.ML	Sun Nov 11 20:31:46 2012 +0100
@@ -153,16 +153,15 @@
 val flexflex_tac = PRIMSEQ Thm.flexflex_rule;
 
 (*Remove duplicate subgoals.*)
-val perm_tac = PRIMITIVE oo Thm.permute_prems;
-
+val permute_tac = PRIMITIVE oo Thm.permute_prems;
 fun distinct_tac (i, k) =
-  perm_tac 0 (i - 1) THEN
-  perm_tac 1 (k - 1) THEN
+  permute_tac 0 (i - 1) THEN
+  permute_tac 1 (k - 1) THEN
   DETERM (PRIMSEQ (fn st =>
     Thm.compose_no_flatten false (st, 0) 1
       (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
-  perm_tac 1 (1 - k) THEN
-  perm_tac 0 (1 - i);
+  permute_tac 1 (1 - k) THEN
+  permute_tac 0 (1 - i);
 
 fun distinct_subgoal_tac i st =
   (case drop (i - 1) (Thm.prems_of st) of