src/HOL/Mutabelle/mutabelle_extra.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36743 ce2297415b54
     1.1 --- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -218,8 +218,8 @@
     1.4  
     1.5  fun is_forbidden_theorem (s, th) =
     1.6    let val consts = Term.add_const_names (prop_of th) [] in
     1.7 -    exists (fn s' => s' mem space_explode "." s) forbidden_thms orelse
     1.8 -    exists (fn s' => s' mem forbidden_consts) consts orelse
     1.9 +    exists (member (op =) (space_explode "." s)) forbidden_thms orelse
    1.10 +    exists (member (op =) forbidden_consts) consts orelse
    1.11      length (space_explode "." s) <> 2 orelse
    1.12      String.isPrefix "type_definition" (List.last (space_explode "." s)) orelse
    1.13      String.isSuffix "_def" s orelse