src/Pure/Syntax/ast.ML

 
 Abstract syntax trees, translation rules, matching and normalization of asts.
 *)
 
 signature AST0 =
-sig
+  sig
   datatype ast =
     Constant of string |
     Variable of string |
     Appl of ast list
   exception AST of string * ast list
-end;
+  end;
 
 signature AST1 =
-sig
+  sig
   include AST0
-  structure Pretty: PRETTY
   val mk_appl: ast -> ast list -> ast
   val str_of_ast: ast -> string
   val pretty_ast: ast -> Pretty.T
   val pretty_rule: ast * ast -> Pretty.T
   val pprint_ast: ast -> pprint_args -> unit
   val trace_norm_ast: bool ref
   val stat_norm_ast: bool ref
-end;
+  end;
 
 signature AST =
-sig
+  sig
   include AST1
   val raise_ast: string -> ast list -> 'a
   val head_of_rule: ast * ast -> string
   val rule_error: ast * ast -> string option
   val fold_ast: string -> ast list -> ast
   val fold_ast_p: string -> ast list * ast -> ast
   val unfold_ast: string -> ast -> ast list
   val unfold_ast_p: string -> ast -> ast list * ast
   val normalize: bool -> bool -> (string -> (ast * ast) list) option -> ast -> ast
   val normalize_ast: (string -> (ast * ast) list) option -> ast -> ast
-end;
-
-functor AstFun(Pretty: PRETTY): AST =
+  end;
+
+structure Ast : AST =
 struct
-
-structure Pretty = Pretty;
-
 
 (** abstract syntax trees **)
 
 (*asts come in two flavours:
    - ordinary asts representing terms and typs: Variables are (often) treated

 (* normalize_ast *)
 
 fun normalize_ast get_rules ast =
   normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast;
 
-
 end;
+