src/Pure/display.ML
changeset 3936 1954255c29ef
parent 3879 de18c0c1141c
child 3990 a8c80f5fdd16
equal deleted inserted replaced
3935:52c14fe8f16b 3936:1954255c29ef
   105   let
   105   let
   106     val {sign, new_axioms, oracles, ...} = rep_theory thy;
   106     val {sign, new_axioms, oracles, ...} = rep_theory thy;
   107     val axioms = Symtab.dest new_axioms;
   107     val axioms = Symtab.dest new_axioms;
   108     val oras = map fst (Symtab.dest oracles);
   108     val oras = map fst (Symtab.dest oracles);
   109 
   109 
   110     fun prt_axm (a, t) = Pretty.block [Pretty.str (a ^ ":"), Pretty.brk 1,
   110     fun prt_axm (a, t) = Pretty.block
   111       Pretty.quote (Sign.pretty_term sign t)];
   111       [Pretty.str (Sign.cond_extern sign Theory.thmK a ^ ":"), Pretty.brk 1,
       
   112         Pretty.quote (Sign.pretty_term sign t)];
   112   in
   113   in
   113     Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
   114     Pretty.writeln (Pretty.big_list "additional axioms:" (map prt_axm axioms));
   114     Pretty.writeln (Pretty.strs ("oracles:" :: oras))
   115     Pretty.writeln (Pretty.strs ("oracles:" :: oras))
   115   end;
   116   end;
   116 
   117