1.1 --- a/src/HOL/Tools/meson.ML Tue May 08 15:37:27 2007 +0200
1.2 +++ b/src/HOL/Tools/meson.ML Tue May 08 17:40:18 2007 +0200
1.3 @@ -240,7 +240,7 @@
1.4 (*Any need to extend this list with
1.5 "HOL.type_class","Code_Generator.eq_class","ProtoPure.term"?*)
1.6 val has_meta_conn =
1.7 - exists_Const (fn (c,_) => c mem_string ["==", "==>", "all", "prop"]);
1.8 + exists_Const (member (op =) ["==", "==>", "all", "prop"] o #1);
1.9
1.10 fun apply_skolem_ths (th, rls) =
1.11 let fun tryall [] = raise THM("apply_skolem_ths", 0, th::rls)