changeset 58852 | 621c052789b4 |
parent 58842 | 22b87ab47d3b |
child 58918 | 8d36bc5eaed3 |
--- 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