Syntax.mk_trfun;

--- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 18:57:18 2005 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 18:57:39 2005 +0200
@@ -371,6 +371,8 @@
 fun prep_struct (x, _, NONE) = SOME x
   | prep_struct _ = NONE;
 
+fun mk trs = map Syntax.mk_trfun trs;
+
 in
 
 fun add_syntax decls =
@@ -384,11 +386,12 @@
       val syn' = syn
         |> Syntax.extend_const_gram is_logtype ("", false) mxs_output
         |> Syntax.extend_const_gram is_logtype ("", true) mxs
-        |> Syntax.extend_trfuns ([], trs, [], []);
-    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
+        |> Syntax.extend_trfuns ([], mk trs, [], []);
+    in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end);
 
 fun syn_of (Context {syntax = (syn, structs, _), ...}) =
-  syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
+  let val (atrs, trs, trs', atrs') = Syntax.struct_trfuns structs
+  in syn |> Syntax.extend_trfuns (mk atrs, mk trs, mk trs', mk atrs') end;
 
 end;
 
@@ -455,8 +458,6 @@
 
 in
 
-(* Read/certify type, using default sort information from context. *)
-
 val read_typ     = read_typ_aux Sign.read_typ';
 val read_typ_raw = read_typ_aux Sign.read_typ_raw';
 val cert_typ     = cert_typ_aux Sign.certify_typ;
@@ -1512,4 +1513,3 @@
 val setup = [ProofDataData.init];
 
 end;
-

--- a/src/Pure/Syntax/type_ext.ML	Sat Apr 16 18:57:18 2005 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Sat Apr 16 18:57:39 2005 +0200
@@ -24,7 +24,7 @@
   val type_ext: SynExt.syn_ext
 end;
 
-structure TypeExt : TYPE_EXT =
+structure TypeExt: TYPE_EXT =
 struct
 
 
@@ -215,10 +215,11 @@
    Mfix ("'(_')",       typeT --> typeT,               "", [0], max_pri),
    Mfix ("'_",          typeT,                         "dummy", [], max_pri)]
   []
-  ([("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
+  (map SynExt.mk_trfun
+   [("_tapp", tapp_ast_tr), ("_tappl", tappl_ast_tr), ("_bracket", bracket_ast_tr)],
    [],
    [],
-   [("fun", fun_ast_tr')])
+   map SynExt.mk_trfun [("fun", fun_ast_tr')])
   TokenTrans.token_translation
   ([], []);