tuned output;
authorwenzelm
Fri, 25 May 2018 21:02:40 +0200
changeset 68274 867bd42b3f59
parent 68273 53788963c4dc
child 68275 b5d0318757f0
tuned output;
src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Fri May 25 21:01:51 2018 +0200
+++ b/src/Pure/Isar/element.ML	Fri May 25 21:02:40 2018 +0200
@@ -171,9 +171,8 @@
       | prt_mixfix mx = [Pretty.brk 2, Mixfix.pretty_mixfix mx];
 
     fun prt_fix (x, SOME T, mx) = Pretty.block (prt_name (Binding.name_of x) :: Pretty.str " ::" ::
-          Pretty.brk 1 :: prt_typ T :: Pretty.brk 1 :: prt_mixfix mx)
-      | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) ::
-          Pretty.brk 1 :: prt_mixfix mx);
+          Pretty.brk 1 :: prt_typ T :: prt_mixfix mx)
+      | prt_fix (x, NONE, mx) = Pretty.block (prt_name (Binding.name_of x) :: prt_mixfix mx);
     fun prt_constrain (x, T) = prt_fix (Binding.name x, SOME T, NoSyn);
 
     fun prt_asm (a, ts) =