# HG changeset patch
# User wenzelm
# Date 1365000314 -7200
# Node ID 4c7fdc00bd5929648969f0ae1945b22fc702a308
# Parent  8e80ecfa3652f7f54cbaa86ed3b35d631ce3a0e4
tuned -- Drule.comp_no_flatten includes Drule.incr_indexes already (NB: result should be deterministic by construction);

diff -r 8e80ecfa3652 -r 4c7fdc00bd59 src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Wed Apr 03 13:58:00 2013 +0200
+++ b/src/Pure/tactic.ML	Wed Apr 03 16:45:14 2013 +0200
@@ -157,9 +157,7 @@
 fun distinct_tac (i, k) =
   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
+  PRIMITIVE (fn st => Drule.comp_no_flatten (st, 0) 1 Drule.distinct_prems_rl) THEN
   permute_tac 1 (1 - k) THEN
   permute_tac 0 (1 - i);