src/HOL/Statespace/state_space.ML

--- a/src/HOL/Statespace/state_space.ML	Wed May 05 09:24:42 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML	Wed May 05 18:25:34 2010 +0200
@@ -528,7 +528,7 @@
             | 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]);