src/HOL/Statespace/state_space.ML

         val err_dup_renamings = (case duplicates (op =) rnames of
              [] => []
             | dups => ["Duplicate renaming(s) for " ^ commas dups])
 
         val cnames = map fst components;
-        val err_rename_unknowns = (case (filter (fn n => not (n mem cnames))) rnames of
+        val err_rename_unknowns = (case subtract (op =) cnames rnames of
               [] => []
              | rs => ["Unknown components " ^ commas rs]);
 
 
         val rs' = map (AList.lookup (op =) rs o fst) components;