diff -r 1bc3b688548c -r fff6f11b1f09 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Nov 24 14:37:23 2009 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Nov 24 17:28:25 2009 +0100
@@ -265,7 +265,7 @@
       if nesting = 0 andalso not (Toplevel.is_proof state) then tag_stack
       else if nesting >= 0 then (tag', replicate nesting tag @ tags)
       else
-        (case Library.drop (~ nesting - 1, tags) of
+        (case (uncurry drop) (~ nesting - 1, tags) of
           tgs :: tgss => (tgs, tgss)
         | [] => err_bad_nesting (Position.str_of cmd_pos));