src/HOL/Import/shuffler.ML

--- a/src/HOL/Import/shuffler.ML	Thu Oct 29 16:59:12 2009 +0100
+++ b/src/HOL/Import/shuffler.ML	Thu Oct 29 17:58:26 2009 +0100
@@ -628,7 +628,7 @@
         val all_thms =
           map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
     in
-        List.filter (match_consts ignored t) all_thms
+        filter (match_consts ignored t) all_thms
     end
 
 fun gen_shuffle_tac ctxt search thms i st =