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

diff -r 192c48376d25 -r f600215b6ea7 src/Pure/Syntax/lexicon.ML
--- a/src/Pure/Syntax/lexicon.ML	Fri Feb 16 14:06:09 1996 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Feb 16 14:17:34 1996 +0100
@@ -10,7 +10,7 @@
 infix 0 ||;
 
 signature SCANNER =
-sig
+  sig
   exception LEXICAL_ERROR
   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
   val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
@@ -37,10 +37,10 @@
   val make_lexicon: string list -> lexicon
   val merge_lexicons: lexicon -> lexicon -> lexicon
   val scan_literal: lexicon -> string list -> string * string list
-end;
+  end;
 
 signature LEXICON0 =
-sig
+  sig
   val is_identifier: string -> bool
   val string_of_vname: indexname -> string
   val scan_varname: string list -> indexname * string list
@@ -48,10 +48,10 @@
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
-end;
+  end;
 
 signature LEXICON =
-sig
+  sig
   include SCANNER
   include LEXICON0
   val is_xid: string -> bool
@@ -78,12 +78,11 @@
   val valued_token: token -> bool
   val predef_term: string -> token option
   val tokenize: lexicon -> bool -> string -> token list
-end;
+  end;
 
-functor LexiconFun(): LEXICON =
+structure Lexicon : LEXICON =
 struct
 
-
 (** is_identifier etc. **)
 
 fun is_ident [] = false
@@ -465,6 +464,5 @@
     #1 (scan (explode str))
   end;
 
-
 end;
 
diff -r 192c48376d25 -r f600215b6ea7 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Feb 16 14:06:09 1996 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 16 14:17:34 1996 +0100
@@ -6,7 +6,7 @@
 *)
 
 signature MIXFIX0 =
-sig
+  sig
   datatype mixfix =
     NoSyn |
     Mixfix of string * int list * int |
@@ -15,10 +15,10 @@
     Infixr of int |
     Binder of string * int * int
   val max_pri: int
-end;
+  end;
 
 signature MIXFIX1 =
-sig
+  sig
   include MIXFIX0
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
@@ -26,25 +26,19 @@
   val pure_syntax: (string * string * mixfix) list
   val pure_appl_syntax: (string * string * mixfix) list
   val pure_applC_syntax: (string * string * mixfix) list
-end;
+  end;
 
 signature MIXFIX =
-sig
+  sig
   include MIXFIX1
-  structure SynExt: SYN_EXT
-  local open SynExt in
-    val syn_ext_types: string list -> (string * int * mixfix) list -> syn_ext
-    val syn_ext_consts: string list -> (string * typ * mixfix) list -> syn_ext
-  end
-end;
+  val syn_ext_types: string list -> (string * int * mixfix) list -> SynExt.syn_ext
+  val syn_ext_consts: string list -> (string * typ * mixfix) list -> SynExt.syn_ext
+  end;
 
-functor MixfixFun(structure Lexicon: LEXICON and SynExt: SYN_EXT
-  and SynTrans: SYN_TRANS): MIXFIX =
+structure Mixfix : MIXFIX =
 struct
 
-structure SynExt = SynExt;
-open Lexicon SynExt SynExt.Ast SynTrans;
-
+open Lexicon SynExt Ast SynTrans;
 
 (** mixfix declarations **)
 
diff -r 192c48376d25 -r f600215b6ea7 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Fri Feb 16 14:06:09 1996 +0100
+++ b/src/Pure/Syntax/parser.ML	Fri Feb 16 14:17:34 1996 +0100
@@ -6,33 +6,24 @@
 *)
 
 signature PARSER =
-sig
-  structure Lexicon: LEXICON
-  structure SynExt: SYN_EXT
-  local open Lexicon SynExt SynExt.Ast in
-    type gram
-    val empty_gram: gram
-    val extend_gram: gram -> xprod list -> gram
-    val merge_grams: gram -> gram -> gram
-    val pretty_gram: gram -> Pretty.T list
-    datatype parsetree =
-      Node of string * parsetree list |
-      Tip of token
-    val parse: gram -> string -> token list -> parsetree list
-  end
-  val branching_level: int ref;
-end;
+  sig
+  type gram
+  val empty_gram: gram
+  val extend_gram: gram -> SynExt.xprod list -> gram
+  val merge_grams: gram -> gram -> gram
+  val pretty_gram: gram -> Pretty.T list
+  datatype parsetree =
+    Node of string * parsetree list |
+    Tip of Lexicon.token
+  val parse: gram -> string -> Lexicon.token list -> parsetree list
+  val branching_level: int ref
+  end;
 
-functor ParserFun(structure Symtab: SYMTAB and Lexicon: LEXICON
-  and SynExt: SYN_EXT): PARSER =
+
+structure Parser : PARSER =
 struct
-
-structure Pretty = SynExt.Ast.Pretty;
-structure Lexicon = Lexicon;
-structure SynExt = SynExt;
 open Lexicon SynExt;
 
-
 (** datatype gram **)
 
 type nt_tag = int;              (*production for the NTs are stored in an array