src/Pure/Thy/thy_syn.ML
changeset 1512 ce37c64244c0
parent 476 836cad329311
child 3619 0fc67ad6d62a
     1.1 --- a/src/Pure/Thy/thy_syn.ML	Fri Feb 16 17:24:51 1996 +0100
     1.2 +++ b/src/Pure/Thy/thy_syn.ML	Fri Feb 16 18:00:47 1996 +0100
     1.3 @@ -6,26 +6,25 @@
     1.4  *)
     1.5  
     1.6  signature THY_SYN_DATA =
     1.7 -sig
     1.8 +  sig
     1.9    val user_keywords: string list
    1.10    val user_sections: (string * (ThyParse.token list -> (string * string)
    1.11      * ThyParse.token list)) list
    1.12 -end;
    1.13 +  end;
    1.14  
    1.15  signature THY_SYN =
    1.16 -sig
    1.17 +  sig
    1.18    val parse: string -> string -> string
    1.19 -end;
    1.20 +  end;
    1.21  
    1.22 -functor ThySynFun(ThySynData: THY_SYN_DATA): THY_SYN =
    1.23 +functor ThySynFun (Data: THY_SYN_DATA): THY_SYN =
    1.24  struct
    1.25  
    1.26 -open ThyParse ThySynData;
    1.27 +val syntax =
    1.28 +  ThyParse.make_syntax (ThyParse.pure_keywords @ Data.user_keywords)
    1.29 +		       (ThyParse.pure_sections @ Data.user_sections);
    1.30  
    1.31 -val syntax =
    1.32 -  make_syntax (pure_keywords @ user_keywords) (pure_sections @ user_sections);
    1.33 -
    1.34 -val parse = parse_thy syntax;
    1.35 +val parse = ThyParse.parse_thy syntax;
    1.36  
    1.37  end;
    1.38