# HG changeset patch
# User wenzelm
# Date 877337461 -7200
# Node ID 1954255c29ef1711c9dcea883224000ea87c5096
# Parent  52c14fe8f16b71c4f6aace2cea465af56506fd4c
tuned output;

diff -r 52c14fe8f16b -r 1954255c29ef src/Pure/display.ML
--- a/src/Pure/display.ML	Mon Oct 20 10:48:22 1997 +0200
+++ b/src/Pure/display.ML	Mon Oct 20 10:51:01 1997 +0200
@@ -107,8 +107,9 @@
     val axioms = Symtab.dest new_axioms;
     val oras = map fst (Symtab.dest oracles);
 
-    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
-      Pretty.quote (Sign.pretty_term sign t)];
+    fun prt_axm (a, t) = Pretty.block
+      [Pretty.str (Sign.cond_extern sign Theory.thmK a ^ ":"), Pretty.brk 1,
+        Pretty.quote (Sign.pretty_term sign t)];
   in
     Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
     Pretty.writeln (Pretty.strs ("oracles:" :: oras))