Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
'notation': allow 'structure' as well;
authorwenzelm
Thu, 11 Oct 2007 00:28:30 +0200
changeset 24953 f92386569176
parent 24952 f336c36f41a0
child 24954 0664f10a4094
'notation': allow 'structure' as well;
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- 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)));
isabelle