# HG changeset patch
# User clasohm
# Date 751324645 -3600
# Node ID e76a1edc2e49c0b8f89bf05cb60d48edbace8cac
# Parent  c94c8ebc0b1588e54675a23a8776041701b2fcb9
removed a bug that occured when a path was specified for use_thy's parameter
and the theory was created in a .ML file

diff -r c94c8ebc0b15 -r e76a1edc2e49 src/Pure/Thy/read.ML
--- a/src/Pure/Thy/read.ML	Fri Oct 22 17:39:12 1993 +0100
+++ b/src/Pure/Thy/read.ML	Fri Oct 22 22:17:25 1993 +0100
@@ -120,7 +120,7 @@
                       then (find_file path (thy ^ ".ML")
                             handle FILE_NOT_FOUND => 
                              error ("Could find no .thy or .ML file for theory "
-                                    ^ name))
+                                    ^ thy_name))
                       else if file_exists (thy_path ^ thy ^ ".ML")
                       then thy_path ^ thy ^ ".ML"
                       else ""
@@ -187,8 +187,8 @@
                  use ml_file;
                  let val outstream = open_out (".tmp.ML") 
                  in
-                    output (outstream, "store_theory " ^ quote name ^ " " ^ name
-                                       ^ ".thy;\n");
+                    output (outstream, "store_theory " ^ quote thy_name ^ " "
+                                       ^ thy_name ^ ".thy;\n");
                     close_out outstream 
                  end;
                  use ".tmp.ML";
@@ -198,7 +198,7 @@
 
          (*Now set the correct info.*)
          (set_info (file_info thy_file) (file_info ml_file) thy
-          handle THY_NOT_FOUND => error ("Could not find theory \"" ^ name
+          handle THY_NOT_FOUND => error ("Could not find theory \"" ^ thy
                                          ^ "\" (wrong filename?)"));
 
          (*Mark theories that have to be reloaded.*)