1.1 --- a/src/Pure/Syntax/syn_ext.ML	Fri Dec 13 17:29:22 1996 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Fri Dec 13 17:30:28 1996 +0100
     1.3 @@ -38,25 +38,27 @@
     1.4        parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
     1.5        parse_rules: (Ast.ast * Ast.ast) list,
     1.6        parse_translation: (string * (term list -> term)) list,
     1.7 -      print_translation: (string * (term list -> term)) list,
     1.8 +      print_translation: (string * (typ -> term list -> term)) list,
     1.9        print_rules: (Ast.ast * Ast.ast) list,
    1.10        print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list}
    1.11    val mk_syn_ext: bool -> string list -> mfix list ->
    1.12      string list -> (string * (Ast.ast list -> Ast.ast)) list *
    1.13      (string * (term list -> term)) list *
    1.14 -    (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.15 +    (string * (typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.16      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.17    val syn_ext: string list -> mfix list -> string list ->
    1.18      (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    1.19 -    (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.20 +    (string * (typ -> term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.21      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.22    val syn_ext_logtypes: string list -> syn_ext
    1.23    val syn_ext_const_names: string list -> string list -> syn_ext
    1.24    val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    1.25 +  val fix_tr': (term list -> term) -> typ -> term list -> term
    1.26    val syn_ext_trfuns: string list ->
    1.27      (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
    1.28      (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
    1.29      -> syn_ext
    1.30 +  val syn_ext_trfunsT: string list -> (string * (typ -> term list -> term)) list -> syn_ext
    1.31    val pure_ext: syn_ext
    1.32    end;
    1.33  
    1.34 @@ -281,7 +283,7 @@
    1.35      parse_ast_translation: (string * (Ast.ast list -> Ast.ast)) list,
    1.36      parse_rules: (Ast.ast * Ast.ast) list,
    1.37      parse_translation: (string * (term list -> term)) list,
    1.38 -    print_translation: (string * (term list -> term)) list,
    1.39 +    print_translation: (string * (typ -> term list -> term)) list,
    1.40      print_rules: (Ast.ast * Ast.ast) list,
    1.41      print_ast_translation: (string * (Ast.ast list -> Ast.ast)) list};
    1.42  
    1.43 @@ -310,6 +312,7 @@
    1.44        print_ast_translation = print_ast_translation}
    1.45    end;
    1.46  
    1.47 +
    1.48  val syn_ext = mk_syn_ext true;
    1.49  
    1.50  fun syn_ext_logtypes logtypes =
    1.51 @@ -321,8 +324,14 @@
    1.52  fun syn_ext_rules logtypes rules =
    1.53    syn_ext logtypes [] [] ([], [], [], []) rules;
    1.54  
    1.55 -fun syn_ext_trfuns logtypes trfuns =
    1.56 -  syn_ext logtypes [] [] trfuns ([], []);
    1.57 +fun fix_tr' f _ args = f args;
    1.58 +
    1.59 +fun syn_ext_trfuns logtypes (atrs, trs, tr's, atr's) =
    1.60 +  syn_ext logtypes [] [] (atrs, trs, map (apsnd fix_tr') tr's, atr's) ([], []);
    1.61 +
    1.62 +fun syn_ext_trfunsT logtypes tr's =
    1.63 +  syn_ext logtypes [] [] ([], [], tr's, []) ([], []);
    1.64 +
    1.65  
    1.66  (* pure_ext *)
    1.67