# HG changeset patch
# User paulson
# Date 824487891 -3600
# Node ID 09354d37a5abf80c4f756831d55ce3425c9f2db5
# Parent  4588ba1b14387ee1bfefecbc8996c42e80b53fd7
Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

diff -r 4588ba1b1438 -r 09354d37a5ab src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Fri Feb 16 17:18:51 1996 +0100
+++ b/src/Pure/Syntax/syn_trans.ML	Fri Feb 16 17:24:51 1996 +0100
@@ -6,47 +6,38 @@
 *)
 
 signature SYN_TRANS0 =
-sig
+  sig
   val eta_contract: bool ref
   val mk_binder_tr: string * string -> string * (term list -> term)
   val mk_binder_tr': string * string -> string * (term list -> term)
   val dependent_tr': string * string -> term list -> term
-end;
+  end;
 
 signature SYN_TRANS1 =
-sig
+  sig
   include SYN_TRANS0
-  structure Parser: PARSER
-  local open Parser.SynExt.Ast in
-    val constrainAbsC: string
-    val pure_trfuns:
-      (string * (ast list -> ast)) list *
+  val constrainAbsC: string
+  val pure_trfuns:
+      (string * (Ast.ast list -> Ast.ast)) list *
       (string * (term list -> term)) list *
       (string * (term list -> term)) list *
-      (string * (ast list -> ast)) list
-  end
-end;
+      (string * (Ast.ast list -> Ast.ast)) list
+  end;
 
 signature SYN_TRANS =
-sig
+  sig
   include SYN_TRANS1
-  local open Parser Parser.SynExt Parser.SynExt.Ast in
-    val abs_tr': term -> term
-    val prop_tr': bool -> term -> term
-    val appl_ast_tr': ast * ast list -> ast
-    val applC_ast_tr': ast * ast list -> ast
-    val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
-    val ast_to_term: (string -> (term list -> term) option) -> ast -> term
-  end
-end;
+  val abs_tr': term -> term
+  val prop_tr': bool -> term -> term
+  val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
+  val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
+  val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
+  val ast_to_term: (string -> (term list -> term) option) -> Ast.ast -> term
+  end;
 
-functor SynTransFun(structure TypeExt: TYPE_EXT and Parser: PARSER
-  sharing TypeExt.SynExt = Parser.SynExt): SYN_TRANS =
+structure SynTrans : SYN_TRANS =
 struct
-
-structure Parser = Parser;
-open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser;
-
+open TypeExt Lexicon Ast SynExt Parser;
 
 (** parse (ast) translations **)
 
@@ -313,5 +304,4 @@
     term_of ast
   end;
 
-
 end;
diff -r 4588ba1b1438 -r 09354d37a5ab src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Feb 16 17:18:51 1996 +0100
+++ b/src/Pure/Syntax/syntax.ML	Fri Feb 16 17:24:51 1996 +0100
@@ -8,7 +8,7 @@
 infix |-> <-| <->;
 
 signature BASIC_SYNTAX =
-sig
+  sig
   include AST0
   include SYN_TRANS0
   include MIXFIX0
@@ -17,10 +17,10 @@
     op |-> of 'a * 'a |
     op <-| of 'a * 'a |
     op <-> of 'a * 'a
-end;
+  end;
 
 signature SYNTAX =
-sig
+  sig
   include AST1
   include LEXICON0
   include SYN_EXT0
@@ -28,7 +28,6 @@
   include SYN_TRANS1
   include MIXFIX1
   include PRINTER0
-  sharing type ast = Parser.SynExt.Ast.ast
   datatype 'a trrule =
     op |-> of 'a * 'a |
     op <-| of 'a * 'a |
@@ -62,18 +61,12 @@
   val simple_string_of_typ: typ -> string
   val simple_pprint_typ: typ -> pprint_args -> unit
   val ambiguity_level: int ref
-end;
+  end;
 
-functor SyntaxFun(structure Symtab: SYMTAB and TypeExt: TYPE_EXT
-  and SynTrans: SYN_TRANS and Mixfix: MIXFIX and Printer: PRINTER
-  sharing Mixfix.SynExt = SynTrans.Parser.SynExt = TypeExt.SynExt = Printer.SynExt)
-  : SYNTAX =
+structure Syntax : SYNTAX =
 struct
 
-structure SynExt = TypeExt.SynExt;
-structure Parser = SynTrans.Parser;
-structure Lexicon = Parser.Lexicon;
-open Lexicon SynExt SynExt.Ast Parser TypeExt SynTrans Mixfix Printer;
+open Lexicon SynExt Ast Parser TypeExt SynTrans Mixfix Printer;
 
 
 (** tables of translation functions **)
diff -r 4588ba1b1438 -r 09354d37a5ab src/Pure/Syntax/type_ext.ML
--- a/src/Pure/Syntax/type_ext.ML	Fri Feb 16 17:18:51 1996 +0100
+++ b/src/Pure/Syntax/type_ext.ML	Fri Feb 16 17:24:51 1996 +0100
@@ -6,28 +6,22 @@
 *)
 
 signature TYPE_EXT0 =
-sig
+  sig
   val raw_term_sorts: term -> (indexname * sort) list
   val typ_of_term: (indexname * sort) list -> (indexname -> sort) -> term -> typ
-end;
+  end;
 
 signature TYPE_EXT =
-sig
+  sig
   include TYPE_EXT0
-  structure SynExt: SYN_EXT
-  local open SynExt SynExt.Ast in
-    val term_of_typ: bool -> typ -> term
-    val tappl_ast_tr': ast * ast list -> ast
-    val type_ext: syn_ext
-  end
-end;
+  val term_of_typ: bool -> typ -> term
+  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
+  val type_ext: SynExt.syn_ext
+  end;
 
-functor TypeExtFun(structure Lexicon: LEXICON and SynExt: SYN_EXT): TYPE_EXT =
+structure TypeExt : TYPE_EXT =
 struct
-
-structure SynExt = SynExt;
-open Lexicon SynExt SynExt.Ast;
-
+open Lexicon SynExt Ast;
 
 (** raw_term_sorts **)
 
@@ -182,5 +176,4 @@
    [("fun", fun_ast_tr')])
   ([], []);
 
-
 end;