src/HOL/Import/shuffler.ML

         val shuffles = ShuffleData.get thy
         val ignored = collect_ignored shuffles []
         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 =
     let
         val thy = ProofContext.theory_of ctxt