tuned output;
authorwenzelm
Mon Oct 20 10:51:01 1997 +0200 (1997-10-20)
changeset 39361954255c29ef
parent 3935 52c14fe8f16b
child 3937 988ce6fbf85b
tuned output;
src/Pure/display.ML
     1.1 --- a/src/Pure/display.ML	Mon Oct 20 10:48:22 1997 +0200
     1.2 +++ b/src/Pure/display.ML	Mon Oct 20 10:51:01 1997 +0200
     1.3 @@ -107,8 +107,9 @@
     1.4      val axioms = Symtab.dest new_axioms;
     1.5      val oras = map fst (Symtab.dest oracles);
     1.6  
     1.7 -    fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
     1.8 -      Pretty.quote (Sign.pretty_term sign t)];
     1.9 +    fun prt_axm (a, t) = Pretty.block
    1.10 +      [Pretty.str (Sign.cond_extern sign Theory.thmK a ^ ":"), Pretty.brk 1,
    1.11 +        Pretty.quote (Sign.pretty_term sign t)];
    1.12    in
    1.13      Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
    1.14      Pretty.writeln (Pretty.strs ("oracles:" :: oras))