src/Pure/Syntax/ast.ML

 (* pretty_ast *)
 
 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 *)
 
 val pprint_ast = Pretty.pprint o pretty_ast;
 
 
 (* 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 *)
 
 fun head_of_ast (Constant a) = Some a

     val passes = ref 0;
     val lookups = ref 0;
     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);
 
     fun try_rules ast ((lhs, rhs) :: pats) =