Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned output;
authorwenzelm
Mon, 20 Oct 1997 10:51:01 +0200
changeset 3936 1954255c29ef
parent 3935 52c14fe8f16b
child 3937 988ce6fbf85b
tuned output;
src/Pure/display.ML file | annotate | diff | comparison | revisions 
--- 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))
isabelle