src/HOL/Tools/inductive_codegen.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36960 01594f816e3a
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -140,7 +140,7 @@
     1.4    fold_aterms (fn Var ((x, _), T) => cons (x, T) | _ => I) tm [];
     1.5  
     1.6  fun get_args _ _ [] = ([], [])
     1.7 -  | get_args is i (x::xs) = (if i mem is then apfst else apsnd) (cons x)
     1.8 +  | get_args is i (x::xs) = (if member (op =) is i then apfst else apsnd) (cons x)
     1.9        (get_args is (i+1) xs);
    1.10  
    1.11  fun merge xs [] = xs
    1.12 @@ -237,7 +237,7 @@
    1.13              end)
    1.14                ps));
    1.15  
    1.16 -fun use_random () = "random_ind" mem !Codegen.mode;
    1.17 +fun use_random () = member (op =) (!Codegen.mode) "random_ind";
    1.18  
    1.19  fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) =
    1.20    let
    1.21 @@ -557,7 +557,7 @@
    1.22  
    1.23  fun mk_extra_defs thy defs gr dep names module ts =
    1.24    fold (fn name => fn gr =>
    1.25 -    if name mem names then gr
    1.26 +    if member (op =) names name then gr
    1.27      else
    1.28        (case get_clauses thy name of
    1.29          NONE => gr
    1.30 @@ -576,7 +576,7 @@
    1.31        val args = List.take (snd (strip_comb u), nparms);
    1.32        val arg_vs = maps term_vs args;
    1.33  
    1.34 -      fun get_nparms s = if s mem names then SOME nparms else
    1.35 +      fun get_nparms s = if member (op =) names s then SOME nparms else
    1.36          Option.map #3 (get_clauses thy s);
    1.37  
    1.38        fun dest_prem (_ $ (Const (@{const_name "op :"}, _) $ t $ u)) =
    1.39 @@ -585,7 +585,7 @@
    1.40              Prem ([t, u], eq, false)
    1.41          | dest_prem (_ $ t) =
    1.42              (case strip_comb t of
    1.43 -              (v as Var _, ts) => if v mem args then Prem (ts, v, false) else Sidecond t
    1.44 +              (v as Var _, ts) => if member (op =) args v then Prem (ts, v, false) else Sidecond t
    1.45              | (c as Const (s, _), ts) =>
    1.46                  (case get_nparms s of
    1.47                    NONE => Sidecond t
    1.48 @@ -704,7 +704,7 @@
    1.49      val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1);
    1.50      val xs' = map (fn Bound i => nth xs (k - i)) ts;
    1.51      fun conv xs js =
    1.52 -      if js mem fs then
    1.53 +      if member (op =) fs js then
    1.54          let
    1.55            val (p, xs') = conv xs (1::js);
    1.56            val (q, xs'') = conv xs' (2::js)