# HG changeset patch
# User wenzelm
# Date 1082624359 -7200
# Node ID 3f9d3d5cd0cdd364e28eecb63d25f210acdb34df
# Parent  f5f2340398f9983460c86534b780f5d91b88ec09
non_typed_tr';

diff -r f5f2340398f9 -r 3f9d3d5cd0cd src/Pure/Syntax/mixfix.ML
--- 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;
 
 
diff -r f5f2340398f9 -r 3f9d3d5cd0cd src/Pure/Syntax/syn_ext.ML
--- 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 ([], []);
diff -r f5f2340398f9 -r 3f9d3d5cd0cd src/Pure/Syntax/syn_trans.ML
--- 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])