# HG changeset patch
# User wenzelm
# Date 1192055310 -7200
# Node ID f9238656917692839c8df7cc254a1a52d869c79e
# Parent  f336c36f41a03ed04a09c9e4e46218aaef12316a
'notation': allow 'structure' as well;

diff -r f336c36f41a0 -r f92386569176 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Oct 10 17:32:00 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 11 00:28:30 2007 +0200
@@ -244,13 +244,13 @@
 
 val _ =
   OuterSyntax.command "notation" "add notation for constants / fixed variables" K.thy_decl
-    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
+    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
     >> (fn ((loc, mode), args) =>
         Toplevel.local_theory loc (Specification.notation_cmd true mode args)));
 
 val _ =
   OuterSyntax.command "no_notation" "delete notation for constants / fixed variables" K.thy_decl
-    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- P.mixfix)
+    (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix)
     >> (fn ((loc, mode), args) =>
         Toplevel.local_theory loc (Specification.notation_cmd false mode args)));