src/Pure/Thy/thy_output.ML
changeset 33955 fff6f11b1f09
parent 33388 d64545e6cba5
child 33957 e9afca2118d4
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Nov 24 14:37:23 2009 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Nov 24 17:28:25 2009 +0100
     1.3 @@ -265,7 +265,7 @@
     1.4        if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
     1.5        else if nesting >= 0 then (tag', replicate nesting tag @ tags)
     1.6        else
     1.7 -        (case Library.drop (~ nesting - 1, tags) of
     1.8 +        (case (uncurry drop) (~ nesting - 1, tags) of
     1.9            tgs :: tgss => (tgs, tgss)
    1.10          | [] => err_bad_nesting (Position.str_of cmd_pos));
    1.11