# HG changeset patch
# User wenzelm
# Date 1281531631 -7200
# Node ID 36afb56ec49ea1d8a9cace5809f3eb859e81fbf2
# Parent  d6afb77b0f6daee82c1451a49e2bce0fa0a95d50
tuned whitespace;

diff -r d6afb77b0f6d -r 36afb56ec49e src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 11 13:39:36 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Aug 11 15:00:31 2010 +0200
@@ -1123,7 +1123,7 @@
 val type_notation = gen_notation (K type_syntax);
 val notation = gen_notation const_syntax;
 
-fun target_type_notation add  mode args phi =
+fun target_type_notation add mode args phi =
   let
     val args' = args |> map_filter (fn (T, mx) =>
       let
diff -r d6afb77b0f6d -r 36afb56ec49e src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Aug 11 13:39:36 2010 +0200
+++ b/src/Pure/Syntax/ast.ML	Wed Aug 11 15:00:31 2010 +0200
@@ -75,8 +75,7 @@
 
 fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
   | pretty_ast (Variable x) = Pretty.str x
-  | pretty_ast (Appl asts) =
-      Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
+  | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
 
 fun pretty_rule (lhs, rhs) =
   Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];