1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 05 22:26:20 2010 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 05 23:07:36 2010 +0200
     1.3 @@ -240,7 +240,10 @@
     1.4      val _ = List.app Thy_Syntax.report_token toks;
     1.5    in
     1.6      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
     1.7 -      [tr] => (tr, true)
     1.8 +      [tr] =>
     1.9 +        if Keyword.is_control (Toplevel.name_of tr) then
    1.10 +          (Toplevel.malformed range_pos "Illegal control command", true)
    1.11 +        else (tr, true)
    1.12      | [] => (Toplevel.ignored range_pos, false)
    1.13      | _ => (Toplevel.malformed range_pos not_singleton, true))
    1.14      handle ERROR msg => (Toplevel.malformed range_pos msg, true)