tuned whitespace;
authorwenzelm
Wed Aug 11 15:00:31 2010 +0200 (2010-08-11 ago)
changeset 3832836afb56ec49e
parent 38327 d6afb77b0f6d
child 38329 16bb1e60204b
tuned whitespace;
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/ast.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Aug 11 13:39:36 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Aug 11 15:00:31 2010 +0200
     1.3 @@ -1123,7 +1123,7 @@
     1.4  val type_notation = gen_notation (K type_syntax);
     1.5  val notation = gen_notation const_syntax;
     1.6  
     1.7 -fun target_type_notation add  mode args phi =
     1.8 +fun target_type_notation add mode args phi =
     1.9    let
    1.10      val args' = args |> map_filter (fn (T, mx) =>
    1.11        let
     2.1 --- a/src/Pure/Syntax/ast.ML	Wed Aug 11 13:39:36 2010 +0200
     2.2 +++ b/src/Pure/Syntax/ast.ML	Wed Aug 11 15:00:31 2010 +0200
     2.3 @@ -75,8 +75,7 @@
     2.4  
     2.5  fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
     2.6    | pretty_ast (Variable x) = Pretty.str x
     2.7 -  | pretty_ast (Appl asts) =
     2.8 -      Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
     2.9 +  | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
    2.10  
    2.11  fun pretty_rule (lhs, rhs) =
    2.12    Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];