--- a/src/Pure/Isar/isar_syn.ML Mon Feb 08 17:33:03 1999 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Feb 08 17:33:24 1999 +0100
@@ -210,7 +210,7 @@
(* use ML text *)
val useP =
- OuterSyntax.parser true "use" "eval ML text from file"
+ OuterSyntax.parser false "use" "eval ML text from file"
(name >> IsarCmd.use);
val mlP =
@@ -511,7 +511,7 @@
val keywords =
["(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
- "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",
+ "?", "[", "]", "and", "as", "binder", "files", "infixl", "infixr", "is",
"output", "{", "|", "}"];
val parsers = [