src/HOL/Tools/meson.ML
changeset 22871 9ffb43b19ec6
parent 22724 3002683a6e0f
child 23262 0fafccb015e6
     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)