src/HOL/Tools/choice_specification.ML

         fun proc_const c =
             let
                 val (_, c') = Type.varify [] c
                 val (cname,ctyp) = dest_Const c'
             in
-                case List.filter (fn t => let val (name,typ) = dest_Const t
+                case filter (fn t => let val (name,typ) = dest_Const t
                                      in name = cname andalso Sign.typ_equiv thy (typ, ctyp)
                                      end) thawed_prop_consts of
                     [] => error ("Specification: No suitable instances of constant \"" ^ Syntax.string_of_term_global thy c ^ "\" found")
                   | [cf] => unvarify cf vmap
                   | _ => error ("Specification: Several variations of \"" ^ Syntax.string_of_term_global thy c ^ "\" found (try applying explicit type constraints)")