src/Pure/Syntax/syn_trans.ML
changeset 1511 09354d37a5ab
parent 1326 1fbf9407757c
child 2698 8bccb3ab4ca4
     1.1 --- a/src/Pure/Syntax/syn_trans.ML	Fri Feb 16 17:18:51 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syn_trans.ML	Fri Feb 16 17:24:51 1996 +0100
     1.3 @@ -6,47 +6,38 @@
     1.4  *)
     1.5  
     1.6  signature SYN_TRANS0 =
     1.7 -sig
     1.8 +  sig
     1.9    val eta_contract: bool ref
    1.10    val mk_binder_tr: string * string -> string * (term list -> term)
    1.11    val mk_binder_tr': string * string -> string * (term list -> term)
    1.12    val dependent_tr': string * string -> term list -> term
    1.13 -end;
    1.14 +  end;
    1.15  
    1.16  signature SYN_TRANS1 =
    1.17 -sig
    1.18 +  sig
    1.19    include SYN_TRANS0
    1.20 -  structure Parser: PARSER
    1.21 -  local open Parser.SynExt.Ast in
    1.22 -    val constrainAbsC: string
    1.23 -    val pure_trfuns:
    1.24 -      (string * (ast list -> ast)) list *
    1.25 +  val constrainAbsC: string
    1.26 +  val pure_trfuns:
    1.27 +      (string * (Ast.ast list -> Ast.ast)) list *
    1.28        (string * (term list -> term)) list *
    1.29        (string * (term list -> term)) list *
    1.30 -      (string * (ast list -> ast)) list
    1.31 -  end
    1.32 -end;
    1.33 +      (string * (Ast.ast list -> Ast.ast)) list
    1.34 +  end;
    1.35  
    1.36  signature SYN_TRANS =
    1.37 -sig
    1.38 +  sig
    1.39    include SYN_TRANS1
    1.40 -  local open Parser Parser.SynExt Parser.SynExt.Ast in
    1.41 -    val abs_tr': term -> term
    1.42 -    val prop_tr': bool -> term -> term
    1.43 -    val appl_ast_tr': ast * ast list -> ast
    1.44 -    val applC_ast_tr': ast * ast list -> ast
    1.45 -    val pt_to_ast: (string -> (ast list -> ast) option) -> parsetree -> ast
    1.46 -    val ast_to_term: (string -> (term list -> term) option) -> ast -> term
    1.47 -  end
    1.48 -end;
    1.49 +  val abs_tr': term -> term
    1.50 +  val prop_tr': bool -> term -> term
    1.51 +  val appl_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.52 +  val applC_ast_tr': Ast.ast * Ast.ast list -> Ast.ast
    1.53 +  val pt_to_ast: (string -> (Ast.ast list -> Ast.ast) option) -> Parser.parsetree -> Ast.ast
    1.54 +  val ast_to_term: (string -> (term list -> term) option) -> Ast.ast -> term
    1.55 +  end;
    1.56  
    1.57 -functor SynTransFun(structure TypeExt: TYPE_EXT and Parser: PARSER
    1.58 -  sharing TypeExt.SynExt = Parser.SynExt): SYN_TRANS =
    1.59 +structure SynTrans : SYN_TRANS =
    1.60  struct
    1.61 -
    1.62 -structure Parser = Parser;
    1.63 -open TypeExt Parser.Lexicon Parser.SynExt.Ast Parser.SynExt Parser;
    1.64 -
    1.65 +open TypeExt Lexicon Ast SynExt Parser;
    1.66  
    1.67  (** parse (ast) translations **)
    1.68  
    1.69 @@ -313,5 +304,4 @@
    1.70      term_of ast
    1.71    end;
    1.72  
    1.73 -
    1.74  end;