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;