changeset 33957 | e9afca2118d4 |
parent 33955 | fff6f11b1f09 |
child 35611 | 07a8904f8fcd |
--- a/src/Pure/tactic.ML Tue Nov 24 17:28:44 2009 +0100 +++ b/src/Pure/tactic.ML Wed Nov 25 09:13:46 2009 +0100 @@ -173,7 +173,7 @@ perm_tac 0 (1 - i); fun distinct_subgoal_tac i st = - (case (uncurry drop) (i - 1, Thm.prems_of st) of + (case drop (i - 1) (Thm.prems_of st) of [] => no_tac st | A :: Bs => st |> EVERY (fold (fn (B, k) =>