--- 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
--- 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];