1.1 --- a/src/Pure/tactic.ML	Wed Apr 03 13:58:00 2013 +0200
     1.2 +++ b/src/Pure/tactic.ML	Wed Apr 03 16:45:14 2013 +0200
     1.3 @@ -157,9 +157,7 @@
     1.4  fun distinct_tac (i, k) =
     1.5    permute_tac 0 (i - 1) THEN
     1.6    permute_tac 1 (k - 1) THEN
     1.7 -  DETERM (PRIMSEQ (fn st =>
     1.8 -    Thm.compose_no_flatten false (st, 0) 1
     1.9 -      (Drule.incr_indexes st Drule.distinct_prems_rl))) THEN
    1.10 +  PRIMITIVE (fn st => Drule.comp_no_flatten (st, 0) 1 Drule.distinct_prems_rl) THEN
    1.11    permute_tac 1 (1 - k) THEN
    1.12    permute_tac 0 (1 - i);
    1.13