# HG changeset patch
# User wenzelm
# Date 1232115605 -3600
# Node ID 53bda11e0d3bfbeb1cd0255d9fde1a780b57d0e1
# Parent  b0e01a48867c5a2724fdcf4a70a976ea6024b0f6
export check_name;

diff -r b0e01a48867c -r 53bda11e0d3b src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Jan 16 12:11:06 2009 +0100
+++ b/src/Pure/Thy/thy_load.ML	Fri Jan 16 15:20:05 2009 +0100
@@ -25,6 +25,7 @@
   val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_thy: Path.T -> string -> Path.T * File.ident
+  val check_name: string -> string -> unit
   val deps_thy: Path.T -> string ->
    {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
   val load_ml: Path.T -> Path.T -> Path.T * File.ident
@@ -95,6 +96,11 @@
     | SOME thy_id => thy_id)
   end;
 
+fun check_name name name' =
+  if name = name' then ()
+  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
+    " does not agree with theory name " ^ quote name');
+
 
 (* theory deps *)
 
@@ -104,9 +110,7 @@
     val text = explode (File.read path);
     val (name', imports, uses) =
       ThyHeader.read (Path.position path) (Source.of_list_limited 8000 text);
-    val _ = name = name' orelse
-      error ("Filename " ^ quote (Path.implode (Path.base path)) ^
-        " does not agree with theory name " ^ quote name');
+    val _ = check_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;