# HG changeset patch
# User wenzelm
# Date 1557409647 -7200
# Node ID 81c6a9a9a791d52f5a84938dabe6a987570b690c
# Parent  5a00e8624488aa94cc382f27c3f411d7db7bb6fa
proper formatting (amending 5076725247fa);

diff -r 5a00e8624488 -r 81c6a9a9a791 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu May 09 15:24:40 2019 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu May 09 15:47:27 2019 +0200
@@ -1503,14 +1503,15 @@
           [Pretty.block (Pretty.breaks (head ::
             flat (separate sep (map (single o prt) xs))))];
   in
-    Pretty.block (Pretty.fbreaks
-      (prt_name name :: Pretty.str ":" ::
-        prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @
-        prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let
-          (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
-        (if forall (null o #2) asms then []
-          else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @
-        prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs))
+    Pretty.block
+      (prt_name name :: Pretty.str ":" :: Pretty.fbrk ::
+        Pretty.fbreaks
+          (prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @
+           prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let
+             (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
+           (if forall (null o #2) asms then []
+            else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @
+           prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs))
   end;
 
 in