src/Pure/pure_syn.ML

--- a/src/Pure/pure_syn.ML	Fri Oct 31 21:20:06 2014 +0100
+++ b/src/Pure/pure_syn.ML	Fri Oct 31 21:35:11 2014 +0100
@@ -10,8 +10,8 @@
 val _ =
   Outer_Syntax.command
     (("theory", Keyword.tag_theory Keyword.thy_begin), @{here}) "begin theory"
-    (Thy_Header.args >> (fn header =>
-      Toplevel.init_theory (fn () => Thy_Info.toplevel_begin_theory Path.current header)));
+    (Thy_Header.args >>
+      (fn _ => Toplevel.init_theory (fn () => error "Missing theory initialization")));
 
 val _ =
   Outer_Syntax.command