src/Pure/tactic.ML
changeset 33955 fff6f11b1f09
parent 32971 55ba9b6648ef
child 33957 e9afca2118d4
     1.1 --- a/src/Pure/tactic.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/tactic.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -173,7 +173,7 @@
     1.4    perm_tac 0 (1 - i);
     1.5  
     1.6  fun distinct_subgoal_tac i st =
     1.7 -  (case Library.drop (i - 1, Thm.prems_of st) of
     1.8 +  (case (uncurry drop) (i - 1, Thm.prems_of st) of
     1.9      [] => no_tac st
    1.10    | A :: Bs =>
    1.11        st |> EVERY (fold (fn (B, k) =>