src/HOL/Statespace/state_space.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36958 ad5313f1bd30
     1.1 --- a/src/HOL/Statespace/state_space.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -528,7 +528,7 @@
     1.4              | dups => ["Duplicate renaming(s) for " ^ commas dups])
     1.5  
     1.6          val cnames = map fst components;
     1.7 -        val err_rename_unknowns = (case (filter (fn n => not (n mem cnames))) rnames of
     1.8 +        val err_rename_unknowns = (case subtract (op =) cnames rnames of
     1.9                [] => []
    1.10               | rs => ["Unknown components " ^ commas rs]);
    1.11