author | wenzelm |
Tue, 15 Dec 2015 16:01:57 +0100 | |
changeset 61851 | ccf2df82b2d3 |
parent 61850 | e8447e9eb574 |
child 61852 | d273c24b5776 |
--- a/src/Pure/Isar/attrib.ML Tue Dec 15 11:34:28 2015 +0100 +++ b/src/Pure/Isar/attrib.ML Tue Dec 15 16:01:57 2015 +0100 @@ -167,9 +167,6 @@ (* pretty printing *) -fun markup_extern ctxt = - Name_Space.markup_extern ctxt (Name_Space.space_of_table (get_attributes ctxt)); - fun pretty_attribs _ [] = [] | pretty_attribs ctxt srcs = [Pretty.enum "," "[" "]" (map (Token.pretty_src ctxt) srcs)];