# HG changeset patch
# User wenzelm
# Date 936213352 -7200
# Node ID bd819d0255e15ce40fcfc38e8dcf6a8f9fade10e
# Parent  9bc7797d1249c6a3e2fd08fd356b78952af02c73
replaced IsarCmd.kill_theory by Toplevel.kill;
fix: common constraints;
removed "*" keyword;

diff -r 9bc7797d1249 -r bd819d0255e1 src/Pure/Isar/isar_syn.ML
--- 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", "{", "|",
   "}"];