src/Pure/Isar/isar_syn.ML

   OuterSyntax.command "end" "end current excursion" K.thy_end
     (Scan.succeed (Toplevel.print o Toplevel.exit));
 
 val kill_excursionP =
   OuterSyntax.improper_command "kill" "kill current excursion" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.kill_theory));
+    (Scan.succeed (Toplevel.print o Toplevel.kill));
 
 val contextP =
   OuterSyntax.improper_command "context" "switch theory context" K.thy_switch
     (P.name >> (Toplevel.print oo IsarThy.context));
 

       (P.$$$ "==" |-- P.termp)) >> P.triple1) -- P.marg_comment
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
 
 val fixP =
   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
-    (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
+    (P.and_list1 (Scan.repeat1 P.name -- Scan.option (P.$$$ "::" |-- P.typ) -- P.marg_comment)
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
 
 val letP =
   OuterSyntax.command "let" "bind text variables" K.prf_decl
     (P.and_list1 (P.enum1 "as" P.term -- (P.$$$ "=" |-- P.term) -- P.marg_comment)

 
 (*keep keywords consistent with the parsers, including those in
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
 val keywords =
- ["!", "!!", "%", "%%", "(", ")", "*", "+", ",", "--", ":", "::", ";",
-  "<", "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
+ ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
+  "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
   "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
   "}"];
 
 val parsers = [
   (*theory structure*)