tuned signature;

--- a/src/Pure/Isar/toplevel.ML	Thu Jul 22 18:08:39 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Jul 22 20:36:41 2010 +0200
@@ -632,7 +632,7 @@
 fun run_command thy_name tr st =
   (case
       (case init_of tr of
-        SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) ()
+        SOME name => Exn.capture (fn () => Thy_Load.consistent_name thy_name name) ()
       | NONE => Exn.Result ()) of
     Exn.Result () =>
       let val int = is_some (init_of tr) in

--- a/src/Pure/Thy/thy_load.ML	Thu Jul 22 18:08:39 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Jul 22 20:36:41 2010 +0200
@@ -22,10 +22,10 @@
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
   val split_thy_path: Path.T -> Path.T * string
+  val consistent_name: string -> string -> unit
   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, imports: string list, uses: Path.T list}
   val load_ml: Path.T -> Path.T -> Path.T * File.ident
@@ -75,6 +75,11 @@
     (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
   | _ => error ("Bad theory file specification " ^ Path.implode path));
 
+fun consistent_name name name' =
+  if name = name' then ()
+  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
+    " does not agree with theory name " ^ quote name');
+
 
 (* check files *)
 
@@ -103,11 +108,6 @@
     | 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 *)
 
@@ -117,7 +117,7 @@
     val text = File.read path;
     val (name', imports, uses) =
       Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
-    val _ = check_name name name';
+    val _ = consistent_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;