src/Pure/Thy/thy_read.ML

 (*  Title:      Pure/Thy/thy_read.ML
     ID:         $Id$
-    Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson
+    Author:     Sonia Mahjoub / Tobias Nipkow / L C Paulson / Carsten Clasohm
     Copyright   1993  TU Muenchen
 
 Reading and writing the theory definition files.
 
 For theory XXX, the  input file is called XXX.thy

 datatype thy_info = ThyInfo of {name: string, path: string,
                                 children: string list,
                                 thy_info: string option, ml_info: string option,
                                 theory: Thm.theory option};
 
-signature THY_READ =
+signature READTHY =
 sig
   datatype basetype = Thy  of string
                     | File of string
 
   val loaded_thys    : thy_info list ref

   val base_on        : basetype list -> string -> Thm.theory
   val store_theory   : string -> Thm.theory -> unit
 end;
 
 
-functor ThyReadFun(structure ThyParse: THY_PARSE): THY_READ =
+functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY =
 struct
 
 datatype basetype = Thy  of string
                   | File of string;
 

 fun out_name thy = "." ^ thy ^ ".thy.ML";
 
 (*Read a file specified by thy_file containing theory thy *)
 fun read_thy thy thy_file =
   let 
-    open ThyParse;
     val instream  = open_in thy_file;
     val outstream = open_out (out_name thy);
   in  
-    output (outstream, parse_thy pure_syntax (input (instream, 999999)));
+    output (outstream, ThySyn.parse (input (instream, 999999)));
     close_out outstream;
     close_in instream
   end;
 
 fun file_exists file =