# HG changeset patch
# User wenzelm
# Date 912690604 -3600
# Node ID 6da9ae6d40f5cbe7d6c849a0d45bfa937cac928b
# Parent  1894bfc4aee96c30423d08655c5a70d87833fdc4
and_list;

diff -r 1894bfc4aee9 -r 6da9ae6d40f5 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Dec 03 10:45:06 1998 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Dec 03 14:10:04 1998 +0100
@@ -297,17 +297,17 @@
 
 val assumeP =
   OuterSyntax.parser false "assume" "assume propositions"
-    (opt_thm_name ":" -- Scan.repeat1 propp >>
+    (opt_thm_name ":" -- and_list1 propp >>
       (fn ((x, y), z) => Toplevel.print o Toplevel.proof (IsarThy.assume x y z)));
 
 val fixP =
   OuterSyntax.parser false "fix" "fix variables (Skolem constants)"
-    (Scan.repeat1 (name -- Scan.option ($$$ "::" |-- typ))
+    (and_list1 (name -- Scan.option ($$$ "::" |-- typ))
       >> (fn xs => Toplevel.print o Toplevel.proof (IsarThy.fix xs)));
 
 val letP =
   OuterSyntax.parser false "let" "bind text variables"
-    (enum1 "and" (enum1 "as" term -- ($$$ "=" |-- term))
+    (and_list1 (enum1 "as" term -- ($$$ "=" |-- term))
       >> (fn bs => Toplevel.print o Toplevel.proof (IsarThy.match_bind bs)));
 
 
@@ -508,7 +508,7 @@
 val keywords =
  ["(", ")", "*", "+", "--", ",", ":", "::", ";", "<", "<=", "=", "==", "=>",
   "?", "[", "]", "and", "as", "binder", "infixl", "infixr", "is",
-  "mixfix", "output", "{", "|", "}"];
+  "output", "{", "|", "}"];
 
 val parsers = [
   (*theory structure*)
diff -r 1894bfc4aee9 -r 6da9ae6d40f5 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Thu Dec 03 10:45:06 1998 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Thu Dec 03 14:10:04 1998 +0100
@@ -30,6 +30,8 @@
   val enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
   val list: (token list -> 'a * token list) -> token list -> 'a list * token list
   val list1: (token list -> 'a * token list) -> token list -> 'a list * token list
+  val and_list: (token list -> 'a * token list) -> token list -> 'a list * token list
+  val and_list1: (token list -> 'a * token list) -> token list -> 'a list * token list
   val name: token list -> bstring * token list
   val xname: token list -> xstring * token list
   val text: token list -> string * token list
@@ -133,6 +135,9 @@
 fun list1 scan = enum1 "," scan;
 fun list scan = enum "," scan;
 
+fun and_list1 scan = enum1 "and" scan;
+fun and_list scan = enum "and" scan;
+
 
 (* names and text *)
 
@@ -234,7 +239,7 @@
 fun opt_thm_name s = Scan.optional (thm_name s) ("", []);
 
 val xthm = xname -- opt_attribs;
-val xthms1 = Scan.repeat1 xthm;
+val xthms1 = and_list1 xthm;
 
 
 (* proof methods *)