# HG changeset patch
# User wenzelm
# Date 1215009617 -7200
# Node ID 7d5c4e73c89e8d40772c13329d8754a754d4c69e
# Parent  9b2427cc234e862869a5488fab34bb4848a848cc
Toplevel.init_theory: pass name explicitly;

diff -r 9b2427cc234e -r 7d5c4e73c89e src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 02 16:40:15 2008 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 02 16:40:17 2008 +0200
@@ -324,7 +324,7 @@
 val kill_theory = ThyInfo.if_known_thy ThyInfo.remove_thy;
 
 fun theory (name, imports, uses) =
-  Toplevel.init_theory (begin_theory name imports uses)
+  Toplevel.init_theory name (begin_theory name imports uses)
     (fn thy => (end_theory thy; ()))
     (kill_theory o Context.theory_name);
 
diff -r 9b2427cc234e -r 7d5c4e73c89e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 02 16:40:15 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 02 16:40:17 2008 +0200
@@ -202,7 +202,7 @@
   let
     val result = ref thy;
     val trs = parse (Path.position path) (File.read path);
-    val init = Toplevel.init_theory (K thy) (fn thy' => result := thy') (K ());
+    val init = Toplevel.init_theory "" (K thy) (fn thy' => result := thy') (K ());
     val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]);
   in ! result end;