changeset 33955 | fff6f11b1f09 |
parent 33388 | d64545e6cba5 |
child 33957 | e9afca2118d4 |
--- 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));