diff -r 4860901706db -r 216624270b80 src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Wed Jun 01 15:44:56 1994 +0200
+++ b/src/Pure/Thy/thy_read.ML	Wed Jun 01 15:46:11 1994 +0200
@@ -1,6 +1,6 @@
 (*  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.
@@ -15,7 +15,7 @@
                                 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
@@ -33,7 +33,7 @@
 end;
 
 
-functor ThyReadFun(structure ThyParse: THY_PARSE): THY_READ =
+functor ReadthyFUN(structure ThySyn: THY_SYN): READTHY =
 struct
 
 datatype basetype = Thy  of string
@@ -53,11 +53,10 @@
 (*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;