tuned output;
authorwenzelm
Fri May 25 21:02:40 2018 +0200 (21 months ago)
changeset 68274867bd42b3f59
parent 68273 53788963c4dc
child 68275 b5d0318757f0
tuned output;
src/Pure/Isar/element.ML
     1.1 --- a/src/Pure/Isar/element.ML	Fri May 25 21:01:51 2018 +0200
     1.2 +++ b/src/Pure/Isar/element.ML	Fri May 25 21:02:40 2018 +0200
     1.3 @@ -171,9 +171,8 @@
     1.4        | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
     1.5  
     1.6      fun prt_fix (x, SOME T, mx) = Pretty.block (prt_name (Binding.name_of x) :: Pretty.str " ::" ::
     1.7 -          Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
     1.8 -      | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) ::
     1.9 -          Pretty.brk 1 :: prt_mixfix mx);
    1.10 +          Pretty.brk 1 :: prt_typ T :: prt_mixfix mx)
    1.11 +      | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) :: prt_mixfix mx);
    1.12      fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
    1.13  
    1.14      fun prt_asm (a, ts) =