src/Pure/Syntax/type_ext.ML
changeset 1511 09354d37a5ab
parent 764 b60e77395d1a
child 2438 b630fded4566
     1.1 --- a/src/Pure/Syntax/type_ext.ML	Fri Feb 16 17:18:51 1996 +0100
     1.2 +++ b/src/Pure/Syntax/type_ext.ML	Fri Feb 16 17:24:51 1996 +0100
     1.3 @@ -6,28 +6,22 @@
     1.4  *)
     1.5  
     1.6  signature TYPE_EXT0 =
     1.7 -sig
     1.8 +  sig
     1.9    val raw_term_sorts: term -> (indexname * sort) list
    1.10    val typ_of_term: (indexname * sort) list -> (indexname -> sort) -> term -> typ
    1.11 -end;
    1.12 +  end;
    1.13  
    1.14  signature TYPE_EXT =
    1.15 -sig
    1.16 +  sig
    1.17    include TYPE_EXT0
    1.18 -  structure SynExt: SYN_EXT
    1.19 -  local open SynExt SynExt.Ast in
    1.20 -    val term_of_typ: bool -> typ -> term
    1.21 -    val tappl_ast_tr': ast * ast list -> ast
    1.22 -    val type_ext: syn_ext
    1.23 -  end
    1.24 -end;
    1.25 +  val term_of_typ: bool -> typ -> term
    1.26 +  val tappl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.27 +  val type_ext: SynExt.syn_ext
    1.28 +  end;
    1.29  
    1.30 -functor TypeExtFun(structure Lexicon: LEXICON and SynExt: SYN_EXT): TYPE_EXT =
    1.31 +structure TypeExt : TYPE_EXT =
    1.32  struct
    1.33 -
    1.34 -structure SynExt = SynExt;
    1.35 -open Lexicon SynExt SynExt.Ast;
    1.36 -
    1.37 +open Lexicon SynExt Ast;
    1.38  
    1.39  (** raw_term_sorts **)
    1.40  
    1.41 @@ -182,5 +176,4 @@
    1.42     [("fun", fun_ast_tr')])
    1.43    ([], []);
    1.44  
    1.45 -
    1.46  end;