# HG changeset patch
# User wenzelm
# Date 1192055312 -7200
# Node ID 0664f10a4094b247cd5b7e32eea273f676b76db7
# Parent  f9238656917692839c8df7cc254a1a52d869c79e
update_modesyntax: may delete 'structure' notation as well;

diff -r f92386569176 -r 0664f10a4094 src/Pure/Isar/local_syntax.ML
--- a/src/Pure/Isar/local_syntax.ML	Thu Oct 11 00:28:30 2007 +0200
+++ b/src/Pure/Isar/local_syntax.ML	Thu Oct 11 00:28:32 2007 +0200
@@ -98,8 +98,12 @@
     [] => syntax
   | decls =>
       let
-        val mixfixes' = rev (map_filter (prep_mixfix (add, mode)) decls) @ mixfixes;
-        val structs' = structs @ map_filter prep_struct decls;
+        val new_mixfixes = map_filter (prep_mixfix (add, mode)) decls;
+        val new_structs = map_filter prep_struct decls;
+        val mixfixes' = rev new_mixfixes @ mixfixes;
+        val structs' =
+          if add then structs @ new_structs
+          else subtract (op =) new_structs structs;
         val fixes' = fold (fn ((x, true), _) => cons x | _ => I) mixfixes' [];
       in build_syntax thy mode mixfixes' (structs', fixes') end);