src/Pure/Thy/thy_scan.ML
changeset 1512 ce37c64244c0
parent 978 f7011b47ac38
child 2151 000767995143
     1.1 --- a/src/Pure/Thy/thy_scan.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_scan.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -6,17 +6,17 @@
     1.4  *)
     1.5  
     1.6  signature THY_SCAN =
     1.7 -sig
     1.8 +  sig
     1.9    datatype token_kind =
    1.10      Keyword | Ident | LongIdent | TypeVar | Nat | String | Verbatim | EOF
    1.11    val name_of_kind: token_kind -> string
    1.12    type lexicon
    1.13    val make_lexicon: string list -> lexicon
    1.14    val tokenize: lexicon -> string -> (token_kind * string * int) list
    1.15 -end;
    1.16 +  end;
    1.17  
    1.18  
    1.19 -functor ThyScanFun(Scanner: SCANNER): THY_SCAN =
    1.20 +structure ThyScan : THY_SCAN =
    1.21  struct
    1.22  
    1.23  open Scanner;