src/HOL/Tools/Qelim/cooper.ML
changeset 36692 54b64d4ad524
parent 36527 68a837d1a754
child 36717 2a72455be88b
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -538,6 +538,8 @@
     1.4  
     1.5  open Generated_Cooper;
     1.6  
     1.7 +fun member eq = Library.member eq;
     1.8 +
     1.9  fun cooper s = raise Cooper.COOPER ("Cooper oracle failed", ERROR s);
    1.10  fun i_of_term vs t = case t
    1.11   of Free (xn, xT) => (case AList.lookup (op aconv) vs t
    1.12 @@ -593,12 +595,12 @@
    1.13  in
    1.14  fun term_bools acc t =
    1.15  case t of
    1.16 -    (l as f $ a) $ b => if ty t orelse f mem ops then term_bools (term_bools acc l)b
    1.17 +    (l as f $ a) $ b => if ty t orelse member (op =) ops f then term_bools (term_bools acc l)b
    1.18              else insert (op aconv) t acc
    1.19 -  | f $ a => if ty t orelse f mem ops then term_bools (term_bools acc f) a
    1.20 +  | f $ a => if ty t orelse member (op =) ops f then term_bools (term_bools acc f) a
    1.21              else insert (op aconv) t acc
    1.22    | Abs p => term_bools acc (snd (variant_abs p))
    1.23 -  | _ => if ty t orelse t mem ops then acc else insert (op aconv) t acc
    1.24 +  | _ => if ty t orelse member (op =) ops t then acc else insert (op aconv) t acc
    1.25  end;
    1.26  
    1.27  fun myassoc2 l v =