src/Pure/Syntax/mixfix.ML
changeset 42287 d98eb048a2e4
parent 42284 326f57825e1a
child 42288 2074b31650e6
--- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:05:31 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 14:20:57 2011 +0200
@@ -4,7 +4,7 @@
 Mixfix declarations, infixes, binders.
 *)
 
-signature MIXFIX0 =
+signature BASIC_MIXFIX =
 sig
   datatype mixfix =
     NoSyn |
@@ -15,22 +15,16 @@
     Infixr of string * int |
     Binder of string * int * int |
     Structure
-  val binder_name: string -> string
 end;
 
-signature MIXFIX1 =
+signature MIXFIX =
 sig
-  include MIXFIX0
-  val no_syn: 'a * 'b -> 'a * 'b * mixfix
+  include BASIC_MIXFIX
   val pretty_mixfix: mixfix -> Pretty.T
   val mixfix_args: mixfix -> int
   val mixfixT: mixfix -> typ
   val make_type: int -> typ
-end;
-
-signature MIXFIX =
-sig
-  include MIXFIX1
+  val binder_name: string -> string
   val syn_ext_types: (string * typ * mixfix) list -> Syn_Ext.syn_ext
   val syn_ext_consts: (string -> bool) -> (string * typ * mixfix) list -> Syn_Ext.syn_ext
 end;
@@ -38,7 +32,6 @@
 structure Mixfix: MIXFIX =
 struct
 
-
 (** mixfix declarations **)
 
 datatype mixfix =
@@ -51,8 +44,6 @@
   Binder of string * int * int |
   Structure;
 
-fun no_syn (x, y) = (x, y, NoSyn);
-
 
 (* pretty_mixfix *)
 
@@ -164,3 +155,7 @@
   end;
 
 end;
+
+structure Basic_Mixfix: BASIC_MIXFIX = Mixfix;
+open Basic_Mixfix;
+