src/HOL/Tools/inductive_realizer.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36744 6e1f3d609a68
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5  fun relevant_vars prop = List.foldr (fn
     1.6        (Var ((a, i), T), vs) => (case strip_type T of
     1.7 -        (_, Type (s, _)) => if s mem [@{type_name bool}] then (a, T) :: vs else vs
     1.8 +        (_, Type (s, _)) => if s = @{type_name bool} then (a, T) :: vs else vs
     1.9        | _ => vs)
    1.10      | (_, vs) => vs) [] (OldTerm.term_vars prop);
    1.11  
    1.12 @@ -90,7 +90,7 @@
    1.13            val xs = map (pair "x") Ts;
    1.14            val u = list_comb (t, map Bound (i - 1 downto 0))
    1.15          in 
    1.16 -          if a mem vs then
    1.17 +          if member (op =) vs a then
    1.18              list_abs (("r", U) :: xs, mk_rlz U $ Bound i $ u)
    1.19            else list_abs (xs, mk_rlz Extraction.nullT $ Extraction.nullt $ u)
    1.20          end
    1.21 @@ -257,7 +257,7 @@
    1.22    let
    1.23      val rvs = map fst (relevant_vars (prop_of rule));
    1.24      val xs = rev (Term.add_vars (prop_of rule) []);
    1.25 -    val vs1 = map Var (filter_out (fn ((a, _), _) => a mem rvs) xs);
    1.26 +    val vs1 = map Var (filter_out (fn ((a, _), _) => member (op =) rvs a) xs);
    1.27      val rlzvs = rev (Term.add_vars (prop_of rrule) []);
    1.28      val vs2 = map (fn (ixn, _) => Var (ixn, (the o AList.lookup (op =) rlzvs) ixn)) xs;
    1.29      val rs = map Var (subtract (op = o pairself fst) xs rlzvs);
    1.30 @@ -292,7 +292,7 @@
    1.31        Sign.root_path |>
    1.32        Sign.add_path (Long_Name.implode prfx);
    1.33      val (ty_eqs, rlz_eqs) = split_list
    1.34 -      (map (fn (s, rs) => mk_realizes_eqn (not (s mem rsets)) vs nparms rs) rss);
    1.35 +      (map (fn (s, rs) => mk_realizes_eqn (not (member (op =) rsets s)) vs nparms rs) rss);
    1.36  
    1.37      val thy1' = thy1 |>
    1.38        Theory.copy |>
    1.39 @@ -300,7 +300,7 @@
    1.40        fold (fn s => AxClass.axiomatize_arity
    1.41          (s, replicate ar HOLogic.typeS, HOLogic.typeS)) tnames |>
    1.42          Extraction.add_typeof_eqns_i ty_eqs;
    1.43 -    val dts = map_filter (fn (s, rs) => if s mem rsets then
    1.44 +    val dts = map_filter (fn (s, rs) => if member (op =) rsets s then
    1.45        SOME (dt_of_intrs thy1' vs nparms rs) else NONE) rss;
    1.46  
    1.47      (** datatype representing computational content of inductive set **)
    1.48 @@ -363,7 +363,7 @@
    1.49  
    1.50      (** realizer for induction rule **)
    1.51  
    1.52 -    val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then
    1.53 +    val Ps = map_filter (fn _ $ M $ P => if member (op =) rsets (pred_of M) then
    1.54        SOME (fst (fst (dest_Var (head_of P)))) else NONE)
    1.55          (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
    1.56  
    1.57 @@ -471,7 +471,7 @@
    1.58              list_comb (c, map Var (subtract (op =) params' (rev (Term.add_vars (prop_of rule) []))))))
    1.59                (maps snd rss ~~ #intrs ind_info ~~ rintrs ~~ flat constrss))) thy4;
    1.60      val elimps = map_filter (fn ((s, intrs), p) =>
    1.61 -      if s mem rsets then SOME (p, intrs) else NONE)
    1.62 +      if member (op =) rsets s then SOME (p, intrs) else NONE)
    1.63          (rss' ~~ (elims ~~ #elims ind_info));
    1.64      val thy6 =
    1.65        fold (fn p as (((((elim, _), _), _), _), _) =>