src/Pure/display.ML
changeset 8458 883b28065841
parent 8402 84ff2d1f9a2c
child 8720 840c75ab2a7f
equal deleted inserted replaced
8457:c5eb14ba754c 8458:883b28065841
   174 
   174 
   175     fun pretty_default S = Pretty.block
   175     fun pretty_default S = Pretty.block
   176       [Pretty.str "default:", Pretty.brk 1, prt_sort S];
   176       [Pretty.str "default:", Pretty.brk 1, prt_sort S];
   177 
   177 
   178     fun pretty_ty (t, n) = Pretty.block
   178     fun pretty_ty (t, n) = Pretty.block
   179       [Pretty.str t, Pretty.spc 1, Pretty.str (string_of_int n)];
   179       [Pretty.str t, Pretty.brk 1, Pretty.str (string_of_int n)];
   180 
   180 
   181     fun pretty_log_types ts = Pretty.block
   181     fun pretty_log_types ts = Pretty.block
   182       (Pretty.breaks (Pretty.str "logical types:" :: map Pretty.str ts));
   182       (Pretty.breaks (Pretty.str "logical types:" :: map Pretty.str ts));
   183 
   183 
   184     fun pretty_witness None = Pretty.str "universal non-emptiness witness: --"
   184     fun pretty_witness None = Pretty.str "universal non-emptiness witness: --"