--- 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;