src/HOL/Tools/Qelim/presburger.ML
changeset 36692 54b64d4ad524
parent 35625 9c818cab0dd0
child 36717 2a72455be88b
     1.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -67,9 +67,9 @@
     1.4   | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t
     1.5  
     1.6   fun ty cts t = 
     1.7 - if not (typ_of (ctyp_of_term t) mem [HOLogic.intT, HOLogic.natT, HOLogic.boolT]) then false 
     1.8 + if not (member (op =) [HOLogic.intT, HOLogic.natT, HOLogic.boolT] (typ_of (ctyp_of_term t))) then false 
     1.9      else case term_of t of 
    1.10 -      c$l$r => if c mem [@{term"op *::int => _"}, @{term"op *::nat => _"}] 
    1.11 +      c$l$r => if member (op =) [@{term"op *::int => _"}, @{term"op *::nat => _"}] c
    1.12                 then not (isnum l orelse isnum r)
    1.13                 else not (member (op aconv) cts c)
    1.14      | c$_ => not (member (op aconv) cts c)
    1.15 @@ -85,8 +85,8 @@
    1.16  in 
    1.17  fun is_relevant ctxt ct = 
    1.18   subset (op aconv) (term_constants (term_of ct) , snd (CooperData.get ctxt))
    1.19 - andalso forall (fn Free (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_frees (term_of ct))
    1.20 - andalso forall (fn Var (_,T) => T mem [@{typ "int"}, @{typ nat}]) (OldTerm.term_vars (term_of ct));
    1.21 + andalso forall (fn Free (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_frees (term_of ct))
    1.22 + andalso forall (fn Var (_,T) => member (op =) [@{typ int}, @{typ nat}] T) (OldTerm.term_vars (term_of ct));
    1.23  
    1.24  fun int_nat_terms ctxt ct =
    1.25   let