# HG changeset patch
# User wenzelm
# Date 758985203 -3600
# Node ID 775dd81a58e55f5114df3a4a19592f0b78415785
# Parent  1b3bee8d5d7e205d96f12b9191bbe63bd488e10a
cosmetic changes;

diff -r 1b3bee8d5d7e -r 775dd81a58e5 src/Pure/Syntax/README
--- a/src/Pure/Syntax/README	Wed Jan 19 14:12:40 1994 +0100
+++ b/src/Pure/Syntax/README	Wed Jan 19 14:13:23 1994 +0100
@@ -5,9 +5,10 @@
 following structures are supposed to be exported:
 
   Pretty        (generic pretty printing module)
+  Scanner       (generic scanner toolbox)
+
   Syntax        (interface to the syntax module)
   BasicSyntax   (part of Syntax made pervasive)
-  Scanner       (generic scanner toolbox)
 
 There is no Makefile to compile these files separately; they are compiled as
 part of Pure Isabelle.
diff -r 1b3bee8d5d7e -r 775dd81a58e5 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Wed Jan 19 14:12:40 1994 +0100
+++ b/src/Pure/Syntax/ast.ML	Wed Jan 19 14:13:23 1994 +0100
@@ -84,8 +84,7 @@
 fun pretty_ast (Constant a) = Pretty.str (quote a)
   | pretty_ast (Variable x) = Pretty.str x
   | pretty_ast (Appl asts) =
-      Pretty.blk (2, (Pretty.str "(") ::
-        (separate (Pretty.brk 1) (map pretty_ast asts)) @ [Pretty.str ")"]);
+      Pretty.parents "(" ")" (Pretty.breaks (map pretty_ast asts));
 
 
 (* pprint_ast *)
@@ -96,8 +95,7 @@
 (* pretty_rule *)
 
 fun pretty_rule (lhs, rhs) =
-  Pretty.blk
-    (2, [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs]);
+  Pretty.block [pretty_ast lhs, Pretty.str "  ->", Pretty.brk 2, pretty_ast rhs];
 
 
 (* head_of_ast, head_of_rule *)
@@ -212,8 +210,6 @@
     val failed_matches = ref 0;
     val changes = ref 0;
 
-    fun inc i = i := ! i + 1;
-
     fun subst _ (ast as Constant _) = ast
       | subst env (Variable x) = Env.get (env, x)
       | subst env (Appl asts) = Appl (map (subst env) asts);