--- 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", "{", "|",
"}"];