src/Pure/Syntax/mixfix.ML

--- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 21:11:29 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 22:40:29 2011 +0200
@@ -110,8 +110,8 @@
 
     val mfix = map mfix_of type_decls;
     val _ = map2 check_args type_decls mfix;
-    val xconsts = map #1 type_decls;
-  in Syntax_Ext.syn_ext (map_filter I mfix) xconsts ([], [], [], []) ([], []) end;
+    val consts = map (fn (t, _, _) => (t, "")) type_decls;
+  in Syntax_Ext.syn_ext (map_filter I mfix) consts ([], [], [], []) ([], []) end;
 
 
 (* syn_ext_consts *)
@@ -143,15 +143,16 @@
       | binder _ = NONE;
 
     val mfix = maps mfix_of const_decls;
-    val xconsts = map #1 const_decls;
     val binders = map_filter binder const_decls;
     val binder_trs = binders
       |> map (Syntax_Ext.stamp_trfun binder_stamp o apsnd K o Syntax_Trans.mk_binder_tr);
     val binder_trs' = binders
       |> map (Syntax_Ext.stamp_trfun binder_stamp o
           apsnd (K o Syntax_Trans.non_typed_tr') o Syntax_Trans.mk_binder_tr' o swap);
+
+    val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
   in
-    Syntax_Ext.syn_ext' is_logtype mfix xconsts ([], binder_trs, binder_trs', []) ([], [])
+    Syntax_Ext.syn_ext' is_logtype mfix consts ([], binder_trs, binder_trs', []) ([], [])
   end;
 
 end;