src/Pure/Isar/element.ML
changeset 19731 581cdbdbba9a
parent 19585 70a1ce3b23ae
child 19777 77929c3d2b74
--- a/src/Pure/Isar/element.ML	Fri May 26 22:20:05 2006 +0200
+++ b/src/Pure/Isar/element.ML	Fri May 26 22:20:05 2006 +0200
@@ -236,8 +236,8 @@
 
 fun pretty_name_atts ctxt (name, atts) sep =
   if name = "" andalso null atts then []
-  else [Pretty.block (Pretty.breaks (Pretty.str (ProofContext.extern_thm ctxt name) ::
-    Args.pretty_attribs ctxt atts @ [Pretty.str sep]))];
+  else [Pretty.block
+    (Pretty.breaks (Pretty.str name :: Args.pretty_attribs ctxt atts @ [Pretty.str sep]))];
 
 
 (* pretty_stmt *)