src/Pure/Syntax/lexicon.ML

--- a/src/Pure/Syntax/lexicon.ML	Fri Feb 16 14:06:09 1996 +0100
+++ b/src/Pure/Syntax/lexicon.ML	Fri Feb 16 14:17:34 1996 +0100
@@ -10,7 +10,7 @@
 infix 0 ||;
 
 signature SCANNER =
-sig
+  sig
   exception LEXICAL_ERROR
   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
   val || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b
@@ -37,10 +37,10 @@
   val make_lexicon: string list -> lexicon
   val merge_lexicons: lexicon -> lexicon -> lexicon
   val scan_literal: lexicon -> string list -> string * string list
-end;
+  end;
 
 signature LEXICON0 =
-sig
+  sig
   val is_identifier: string -> bool
   val string_of_vname: indexname -> string
   val scan_varname: string list -> indexname * string list
@@ -48,10 +48,10 @@
   val const: string -> term
   val free: string -> term
   val var: indexname -> term
-end;
+  end;
 
 signature LEXICON =
-sig
+  sig
   include SCANNER
   include LEXICON0
   val is_xid: string -> bool
@@ -78,12 +78,11 @@
   val valued_token: token -> bool
   val predef_term: string -> token option
   val tokenize: lexicon -> bool -> string -> token list
-end;
+  end;
 
-functor LexiconFun(): LEXICON =
+structure Lexicon : LEXICON =
 struct
 
-
 (** is_identifier etc. **)
 
 fun is_ident [] = false
@@ -465,6 +464,5 @@
     #1 (scan (explode str))
   end;
 
-
 end;