src/Pure/Isar/isar_syn.ML
changeset 7415 bd819d0255e1
parent 7368 6b1b6b7c1df0
child 7462 f738df1d82e1
--- a/src/Pure/Isar/isar_syn.ML	Wed Sep 01 21:14:23 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Sep 01 21:15:52 1999 +0200
@@ -29,7 +29,7 @@
 
 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
@@ -317,7 +317,7 @@
 
 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 =
@@ -567,8 +567,8 @@
   outer_parse.ML, otherwise be prepared for unexpected errors*)
 
 val keywords =
- ["!", "!!", "%", "%%", "(", ")", "*", "+", ",", "--", ":", "::", ";",
-  "<", "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
+ ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
+  "<=", "=", "==", "=>", "?", "[", "]", "and", "as", "binder",
   "concl", "files", "infixl", "infixr", "is", "output", "{", "|",
   "}"];