# HG changeset patch
# User wenzelm
# Date 1216050702 -7200
# Node ID e540ad3fb50a46777a674b511eb914aacc06807d
# Parent  4adce8310643c0223e8d92906704b1b800f3e8ff
adapted IsarCmd.init_theory;

diff -r 4adce8310643 -r e540ad3fb50a src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Jul 14 17:51:41 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jul 14 17:51:42 2008 +0200
@@ -31,7 +31,7 @@
 
 val _ =
   OuterSyntax.command "theory" "begin theory" (K.tag_theory K.thy_begin)
-    (ThyHeader.args >> (Toplevel.print oo IsarCmd.theory));
+    (ThyHeader.args >> (Toplevel.print oo IsarCmd.init_theory));
 
 val _ =
   OuterSyntax.command "end" "end (local) theory" (K.tag_theory K.thy_end)
diff -r 4adce8310643 -r e540ad3fb50a src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 14 17:51:41 2008 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 14 17:51:42 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');
     val _ = Toplevel.excursion (init Toplevel.empty :: trs @ [Toplevel.exit Toplevel.empty]);
   in ! result end;