# HG changeset patch
# User wenzelm
# Date 1450191717 -3600
# Node ID ccf2df82b2d30f3f9a76a4175484306445fdde9b
# Parent  e8447e9eb574233825dd26d72e02c1c1a71aca53
unused;

diff -r e8447e9eb574 -r ccf2df82b2d3 src/Pure/Isar/attrib.ML
--- 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)];