# HG changeset patch
# User wenzelm
# Date 1163726395 -3600
# Node ID dd58f13a8eb4522454094445218eb1935b5f44c8
# Parent  c15bcd87f47cf48ed0d5754bc09637c657b9bd04
'notation': more robust 'and' list;

diff -r c15bcd87f47c -r dd58f13a8eb4 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Fri Nov 17 02:19:54 2006 +0100
+++ b/doc-src/IsarRef/generic.tex	Fri Nov 17 02:19:55 2006 +0100
@@ -29,7 +29,7 @@
   ;
   'abbreviation' target? mode? (constdecl? prop +)
   ;
-  'notation' target? mode? (nameref mixfix +)
+  'notation' target? mode? (nameref mixfix + 'and')
   ;
 
   consts: ((name ('::' type)? structmixfix? | vars) + 'and')
diff -r c15bcd87f47c -r dd58f13a8eb4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Fri Nov 17 02:19:54 2006 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Fri Nov 17 02:19:55 2006 +0100
@@ -218,7 +218,7 @@
 
 val notationP =
   OuterSyntax.command "notation" "variable/constant syntax" K.thy_decl
-    (P.opt_locale_target -- opt_mode -- Scan.repeat1 (P.xname -- P.mixfix)
+    (P.opt_locale_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
     >> (fn ((loc, mode), args) =>
         Toplevel.local_theory loc (Specification.notation mode args)));