src/Pure/Syntax/mixfix.ML

--- a/src/Pure/Syntax/mixfix.ML	Fri Aug 23 15:44:31 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Aug 23 18:38:44 2024 +0200
@@ -182,7 +182,7 @@
 
     val mfix = map mfix_of type_decls;
     val _ = map2 check_args type_decls mfix;
-    val consts = map (fn (t, _, _) => (t, "")) type_decls;
+    val consts = map (fn (t, _, _) => (t, [])) type_decls;
   in Syntax_Ext.syn_ext [] (map_filter I mfix) consts ([], [], [], []) ([], []) end;
 
 
@@ -235,7 +235,9 @@
       |> map (Syntax_Ext.stamp_trfun binder_stamp o
           apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap);
 
-    val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
+    val consts =
+      map (fn (c, b) => (c, [b])) binders @
+      map (fn (c, _, _) => (c, [])) const_decls;
   in Syntax_Ext.syn_ext logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) end;
 
 end;