tuned output;
authorwenzelm
Sun May 03 18:13:15 2015 +0200 (2015-05-03)
changeset 602461f9cd721ece2
parent 60245 79ad597fe699
child 60247 6a5015b096a2
tuned output;
src/Pure/Isar/class.ML
src/Pure/Isar/overloading.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sun May 03 17:52:27 2015 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sun May 03 18:13:15 2015 +0200
     1.3 @@ -588,7 +588,10 @@
     1.4        Pretty.block (Pretty.breaks
     1.5          [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
     1.6            Pretty.str "::", Syntax.pretty_typ lthy ty]);
     1.7 -  in Pretty.keyword1 "instantiation" :: map pr_arity tycos @ map pr_param params end;
     1.8 +  in
     1.9 +    [Pretty.block
    1.10 +      (Pretty.fbreaks (Pretty.keyword1 "instantiation" :: map pr_arity tycos @ map pr_param params))]
    1.11 +  end;
    1.12  
    1.13  fun conclude lthy =
    1.14    let
    1.15 @@ -754,4 +757,3 @@
    1.16    else [];
    1.17  
    1.18  end;
    1.19 -
     2.1 --- a/src/Pure/Isar/overloading.ML	Sun May 03 17:52:27 2015 +0200
     2.2 +++ b/src/Pure/Isar/overloading.ML	Sun May 03 18:13:15 2015 +0200
     2.3 @@ -174,7 +174,10 @@
     2.4        Pretty.block (Pretty.breaks
     2.5          [Pretty.str v, Pretty.str "==", Proof_Context.pretty_const lthy c,
     2.6            Pretty.str "::", Syntax.pretty_typ lthy ty]);
     2.7 -  in Pretty.keyword1 "overloading" :: map pr_operation overloading end;
     2.8 +  in
     2.9 +    [Pretty.block
    2.10 +      (Pretty.fbreaks (Pretty.keyword1 "overloading" :: map pr_operation overloading))]
    2.11 +  end;
    2.12  
    2.13  fun conclude lthy =
    2.14    let