diff -r e18600daa904 -r fdde6af19ba7 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Oct 22 12:45:38 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Tue Oct 22 12:52:25 2024 +0200
@@ -5,21 +5,18 @@
 Mixfix declarations, infixes, binders.
 *)
 
-signature BASIC_MIXFIX =
-sig
-  datatype mixfix =
-    NoSyn |
-    Mixfix of Input.source * int list * int * Position.range |
-    Infix of Input.source * int * Position.range |
-    Infixl of Input.source * int * Position.range |
-    Infixr of Input.source * int * Position.range |
-    Binder of Input.source * int * int * Position.range |
-    Structure of Position.range
-end;
+datatype mixfix =
+  NoSyn |
+  Mixfix of Input.source * int list * int * Position.range |
+  Infix of Input.source * int * Position.range |
+  Infixl of Input.source * int * Position.range |
+  Infixr of Input.source * int * Position.range |
+  Binder of Input.source * int * int * Position.range |
+  Structure of Position.range;
 
 signature MIXFIX =
 sig
-  include BASIC_MIXFIX
+  datatype mixfix = datatype mixfix
   val mixfix: string -> mixfix
   val is_empty: mixfix -> bool
   val is_infix: mixfix -> bool
@@ -42,14 +39,7 @@
 
 (** mixfix declarations **)
 
-datatype mixfix =
-  NoSyn |
-  Mixfix of Input.source * int list * int * Position.range |
-  Infix of Input.source * int * Position.range |
-  Infixl of Input.source * int * Position.range |
-  Infixr of Input.source * int * Position.range |
-  Binder of Input.source * int * int * Position.range |
-  Structure of Position.range;
+datatype mixfix = datatype mixfix;
 
 fun mixfix s = Mixfix (Input.string s, [], 1000, Position.no_range);
 
@@ -280,6 +270,3 @@
   end;
 
 end;
-
-structure Basic_Mixfix: BASIC_MIXFIX = Mixfix;
-open Basic_Mixfix;