src/HOL/Modelcheck/mucke_oracle.ML
changeset 36692 54b64d4ad524
parent 35010 d6e492cea6e4
child 37135 636e6d8645d6
     1.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -921,7 +921,7 @@
     1.4  check_finity gl bl ((t,cl)::r) b =
     1.5  let
     1.6  fun listmem [] _ = true |
     1.7 -listmem (a::r) l = if (a mem l) then (listmem r l) else false;
     1.8 +listmem (a::r) l = if member (op =) l a then (listmem r l) else false;
     1.9  fun snd_listmem [] _ = true |
    1.10  snd_listmem ((a,b)::r) l = if (listmem b l) then (snd_listmem r l) else false;
    1.11  in
    1.12 @@ -966,7 +966,7 @@
    1.13   (ll @ (new_types r))
    1.14  end;
    1.15  in
    1.16 -        if (a mem done)
    1.17 +        if member (op =) done a
    1.18          then (preprocess_td sg b done)
    1.19          else
    1.20          (let