--- a/src/Pure/Syntax/ast.ML Thu Feb 03 13:57:04 1994 +0100
+++ b/src/Pure/Syntax/ast.ML Thu Feb 03 13:59:00 1994 +0100
@@ -7,24 +7,29 @@
signature AST0 =
sig
- structure Pretty: PRETTY
datatype ast =
Constant of string |
Variable of string |
Appl of ast list
+ exception AST of string * ast list
+end;
+
+signature AST1 =
+sig
+ include AST0
+ structure Pretty: PRETTY
val mk_appl: ast -> ast list -> ast
- exception AST of string * ast list
val str_of_ast: ast -> string
val pretty_ast: ast -> Pretty.T
- val pretty_rule: (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
- include AST0
+ include AST1
val raise_ast: string -> ast list -> 'a
val head_of_rule: ast * ast -> string
val rule_error: ast * ast -> string option