diff -r d98eb048a2e4 -r 2074b31650e6 src/Pure/Syntax/local_syntax.ML
--- a/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 14:20:57 2011 +0200
+++ b/src/Pure/Syntax/local_syntax.ML	Fri Apr 08 15:02:11 2011 +0200
@@ -61,8 +61,8 @@
     val (atrs, trs, trs', atrs') = Syntax_Trans.struct_trfuns structs;
     val local_syntax = thy_syntax
       |> Syntax.update_trfuns
-          (map Syntax.mk_trfun atrs, map Syntax.mk_trfun trs,
-           map Syntax.mk_trfun trs', map Syntax.mk_trfun atrs')
+          (map Syntax_Ext.mk_trfun atrs, map Syntax_Ext.mk_trfun trs,
+           map Syntax_Ext.mk_trfun trs', map Syntax_Ext.mk_trfun atrs')
       |> fold update_gram (AList.coalesce (op =) (rev (map snd mixfixes)));
   in make_syntax (thy_syntax, local_syntax, mode, mixfixes, idents) end;