# HG changeset patch
# User wenzelm
# Date 1148674805 -7200
# Node ID 581cdbdbba9abb3a59c16ba8963807b5805faee7
# Parent  8abecd308e601fe81b806a9c0afa7c8786dd0bf7
pretty: do not exterm thm names;

diff -r 8abecd308e60 -r 581cdbdbba9a src/Pure/Isar/element.ML
--- 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 *)