--- a/src/Pure/Syntax/mixfix.ML Thu Apr 22 10:58:54 2004 +0200
+++ b/src/Pure/Syntax/mixfix.ML Thu Apr 22 10:59:19 2004 +0200
@@ -196,7 +196,8 @@
val xconsts = map name_of const_decls;
val binders = mapfilter binder const_decls;
val binder_trs = map SynTrans.mk_binder_tr binders;
- val binder_trs' = map (apsnd SynExt.fix_tr' o SynTrans.mk_binder_tr' o swap) binders;
+ val binder_trs' =
+ map (apsnd SynTrans.non_typed_tr' o SynTrans.mk_binder_tr' o swap) binders;
in SynExt.syn_ext logtypes mfix xconsts ([], binder_trs, binder_trs', []) [] ([], []) end;
--- a/src/Pure/Syntax/syn_ext.ML Thu Apr 22 10:58:54 2004 +0200
+++ b/src/Pure/Syntax/syn_ext.ML Thu Apr 22 10:59:19 2004 +0200
@@ -61,13 +61,11 @@
val syn_ext_logtypes: string list -> syn_ext
val syn_ext_const_names: string list -> string list -> syn_ext
val syn_ext_rules: string list -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
- val fix_tr': (term list -> term) -> bool -> typ -> term list -> term
val syn_ext_trfuns: string list ->
- (string * (Ast.ast list -> Ast.ast)) list * (string * (term list -> term)) list *
- (string * (term list -> term)) list * (string * (Ast.ast list -> Ast.ast)) list
- -> syn_ext
- val syn_ext_trfunsT: string list ->
- (string * (bool -> typ -> term list -> term)) list -> syn_ext
+ (string * (Ast.ast list -> Ast.ast)) list *
+ (string * (term list -> term)) list *
+ (string * (bool -> typ -> term list -> term)) list *
+ (string * (Ast.ast list -> Ast.ast)) list -> syn_ext
val syn_ext_tokentrfuns: string list
-> (string * string * (string -> string * real)) list -> syn_ext
val pure_ext: syn_ext
@@ -364,13 +362,8 @@
fun syn_ext_rules logtypes rules =
syn_ext logtypes [] [] ([], [], [], []) [] rules;
-fun fix_tr' f _ _ ts = f ts;
-
-fun syn_ext_trfuns logtypes (atrs, trs, tr's, atr's) =
- syn_ext logtypes [] [] (atrs, trs, map (apsnd fix_tr') tr's, atr's) [] ([], []);
-
-fun syn_ext_trfunsT logtypes tr's =
- syn_ext logtypes [] [] ([], [], tr's, []) [] ([], []);
+fun syn_ext_trfuns logtypes trfuns =
+ syn_ext logtypes [] [] trfuns [] ([], []);
fun syn_ext_tokentrfuns logtypes tokentrfuns =
syn_ext logtypes [] [] ([], [], [], []) tokentrfuns ([], []);
--- a/src/Pure/Syntax/syn_trans.ML Thu Apr 22 10:58:54 2004 +0200
+++ b/src/Pure/Syntax/syn_trans.ML Thu Apr 22 10:59:19 2004 +0200
@@ -27,6 +27,8 @@
signature SYN_TRANS1 =
sig
include SYN_TRANS0
+ val non_typed_tr': (term list -> term) -> bool -> typ -> term list -> term
+ val non_typed_tr'': ('a -> term list -> term) -> 'a -> bool -> typ -> term list -> term
val constrainAbsC: string
val pure_trfuns:
(string * (Ast.ast list -> Ast.ast)) list *
@@ -172,6 +174,12 @@
(** print (ast) translations **)
+(* types *)
+
+fun non_typed_tr' f _ _ ts = f ts;
+fun non_typed_tr'' f x _ _ ts = f x ts;
+
+
(* application *)
fun appl_ast_tr' (f, []) = raise Ast.AST ("appl_ast_tr'", [f])