# HG changeset patch
# User paulson
# Date 824475969 -3600
# Node ID 192c48376d2518aad463744388aa7f0f213aed62
# Parent  14f4c55bbe9ad71233f1e3069c1a179cded9b564
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

diff -r 14f4c55bbe9a -r 192c48376d25 src/Pure/Syntax/ROOT.ML
--- a/src/Pure/Syntax/ROOT.ML	Fri Feb 16 13:55:29 1996 +0100
+++ b/src/Pure/Syntax/ROOT.ML	Fri Feb 16 14:06:09 1996 +0100
@@ -16,39 +16,8 @@
 use "printer.ML";
 use "syntax.ML";
 
-structure PrivateSyntax =
-struct
-  structure Pretty = PrettyFun();
-  structure Lexicon = LexiconFun();
-  structure Scanner: SCANNER = Lexicon;
-  structure Ast = AstFun(Pretty);
-  structure SynExt = SynExtFun(structure Lexicon = Lexicon and Ast = Ast);
-  structure Parser = ParserFun(structure Symtab = Symtab and Lexicon = Lexicon
-    and SynExt = SynExt);
-  structure TypeExt = TypeExtFun(structure Lexicon = Lexicon and SynExt = SynExt);
-  structure SynTrans = SynTransFun(structure TypeExt = TypeExt and Parser = Parser);
-  structure Mixfix = MixfixFun(structure Lexicon = Lexicon and SynExt = SynExt and
-    SynTrans = SynTrans);
-  structure Printer = PrinterFun(structure Symtab = Symtab and TypeExt = TypeExt
-    and SynTrans = SynTrans);
-  structure Syntax = SyntaxFun(structure Symtab = Symtab and TypeExt = TypeExt
-    and SynTrans = SynTrans and Mixfix = Mixfix and Printer = Printer);
-  structure BasicSyntax: BASIC_SYNTAX = Syntax;
-end;
+(*Hiding: only the most basic features are opened*)
+structure BasicSyntax: BASIC_SYNTAX = Syntax;
+open BasicSyntax;
 
-structure Pretty = PrivateSyntax.Pretty;
-structure Scanner = PrivateSyntax.Scanner;
-structure Syntax = PrivateSyntax.Syntax;
-structure BasicSyntax = PrivateSyntax.BasicSyntax;
-
-(* hide functors; saves space in PolyML *)
-functor PrettyFun() = struct end;
-functor LexiconFun() = struct end;
-functor AstFun() = struct end;
-functor SynExtFun() = struct end;
-functor ParserFun() = struct end;
-functor TypeExtFun() = struct end;
-functor SynTransFun() = struct end;
-functor MixfixFun() = struct end;
-functor PrinterFun() = struct end;
-functor SyntaxFun() = struct end;
+structure Scanner: SCANNER = Lexicon;
diff -r 14f4c55bbe9a -r 192c48376d25 src/Pure/Syntax/ast.ML
--- a/src/Pure/Syntax/ast.ML	Fri Feb 16 13:55:29 1996 +0100
+++ b/src/Pure/Syntax/ast.ML	Fri Feb 16 14:06:09 1996 +0100
@@ -6,18 +6,17 @@
 *)
 
 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
@@ -25,10 +24,10 @@
   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
@@ -39,14 +38,11 @@
   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;
+  end;
 
-functor AstFun(Pretty: PRETTY): AST =
+structure Ast : AST =
 struct
 
-structure Pretty = Pretty;
-
-
 (** abstract syntax trees **)
 
 (*asts come in two flavours:
@@ -293,5 +289,5 @@
 fun normalize_ast get_rules ast =
   normalize (! trace_norm_ast) (! stat_norm_ast) get_rules ast;
 
+end;
 
-end;