src/Pure/Syntax/mixfix.ML

--- a/src/Pure/Syntax/mixfix.ML	Fri Feb 16 14:06:09 1996 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Fri Feb 16 14:17:34 1996 +0100
@@ -6,7 +6,7 @@
 *)
 
 signature MIXFIX0 =
-sig
+  sig
   datatype mixfix =
     NoSyn |
     Mixfix of string * int list * int |
@@ -15,10 +15,10 @@
     Infixr of int |
     Binder of string * int * int
   val max_pri: int
-end;
+  end;
 
 signature MIXFIX1 =
-sig
+  sig
   include MIXFIX0
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
@@ -26,25 +26,19 @@
   val pure_syntax: (string * string * mixfix) list
   val pure_appl_syntax: (string * string * mixfix) list
   val pure_applC_syntax: (string * string * mixfix) list
-end;
+  end;
 
 signature MIXFIX =
-sig
+  sig
   include MIXFIX1
-  structure SynExt: SYN_EXT
-  local open SynExt in
-    val syn_ext_types: string list -> (string * int * mixfix) list -> syn_ext
-    val syn_ext_consts: string list -> (string * typ * mixfix) list -> syn_ext
-  end
-end;
+  val syn_ext_types: string list -> (string * int * mixfix) list -> SynExt.syn_ext
+  val syn_ext_consts: string list -> (string * typ * mixfix) list -> SynExt.syn_ext
+  end;
 
-functor MixfixFun(structure Lexicon: LEXICON and SynExt: SYN_EXT
-  and SynTrans: SYN_TRANS): MIXFIX =
+structure Mixfix : MIXFIX =
 struct
 
-structure SynExt = SynExt;
-open Lexicon SynExt SynExt.Ast SynTrans;
-
+open Lexicon SynExt Ast SynTrans;
 
 (** mixfix declarations **)