src/Pure/Isar/local_syntax.ML

     (syntax as (Syntax {mode, mixfixes, idents = (structs, _), ...})) =
   (case filter_out (fn (_, (_, _, mx)) => mx = NoSyn) raw_decls of
     [] => 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);
 
 val add_syntax = update_syntax true;