proper formatting (amending 5076725247fa);
authorwenzelm
Thu May 09 15:47:27 2019 +0200 (6 months ago)
changeset 7025581c6a9a9a791
parent 70254 5a00e8624488
child 70256 62a6c1257c05
proper formatting (amending 5076725247fa);
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu May 09 15:24:40 2019 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu May 09 15:47:27 2019 +0200
     1.3 @@ -1503,14 +1503,15 @@
     1.4            [Pretty.block (Pretty.breaks (head ::
     1.5              flat (separate sep (map (single o prt) xs))))];
     1.6    in
     1.7 -    Pretty.block (Pretty.fbreaks
     1.8 -      (prt_name name :: Pretty.str ":" ::
     1.9 -        prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @
    1.10 -        prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let
    1.11 -          (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
    1.12 -        (if forall (null o #2) asms then []
    1.13 -          else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @
    1.14 -        prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs))
    1.15 +    Pretty.block
    1.16 +      (prt_name name :: Pretty.str ":" :: Pretty.fbrk ::
    1.17 +        Pretty.fbreaks
    1.18 +          (prt_sect (Pretty.keyword1 "fix") [] (prt_name o Binding.name_of o fst) fixes @
    1.19 +           prt_sect (Pretty.keyword1 "let") [Pretty.keyword2 "and"] prt_let
    1.20 +             (map_filter (fn (xi, SOME t) => SOME (xi, t) | _ => NONE) lets) @
    1.21 +           (if forall (null o #2) asms then []
    1.22 +            else prt_sect (Pretty.keyword1 "assume") [Pretty.keyword2 "and"] prt_asm asms) @
    1.23 +           prt_sect (Pretty.str "subcases:") [] (prt_name o fst) cs))
    1.24    end;
    1.25  
    1.26  in