src/HOL/Tools/Datatype/datatype_realizer.ML
changeset 36692 54b64d4ad524
parent 35845 e5980f0ad025
child 36744 6e1f3d609a68
     1.1 --- a/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_realizer.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -41,16 +41,16 @@
     1.4        else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
     1.5  
     1.6      val rec_result_Ts = map (fn ((i, _), P) =>
     1.7 -      if i mem is then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
     1.8 +      if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
     1.9          (descr ~~ pnames);
    1.10  
    1.11      fun make_pred i T U r x =
    1.12 -      if i mem is then
    1.13 +      if member (op =) is i then
    1.14          Free (List.nth (pnames, i), T --> U --> HOLogic.boolT) $ r $ x
    1.15        else Free (List.nth (pnames, i), U --> HOLogic.boolT) $ x;
    1.16  
    1.17      fun mk_all i s T t =
    1.18 -      if i mem is then list_all_free ([(s, T)], t) else t;
    1.19 +      if member (op =) is i then list_all_free ([(s, T)], t) else t;
    1.20  
    1.21      val (prems, rec_fns) = split_list (flat (fst (fold_map
    1.22        (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
    1.23 @@ -66,7 +66,7 @@
    1.24                    val vs' = filter_out is_unit vs;
    1.25                    val f = mk_Free "f" (map fastype_of vs' ---> rT) j;
    1.26                    val f' = Envir.eta_contract (list_abs_free
    1.27 -                    (map dest_Free vs, if i mem is then list_comb (f, vs')
    1.28 +                    (map dest_Free vs, if member (op =) is i then list_comb (f, vs')
    1.29                        else HOLogic.unit));
    1.30                  in (HOLogic.mk_Trueprop (make_pred i rT T (list_comb (f, vs'))
    1.31                    (list_comb (Const (cname, Ts ---> T), map Free frees))), f')
    1.32 @@ -100,7 +100,7 @@
    1.33          (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names);
    1.34      val r = if null is then Extraction.nullt else
    1.35        foldr1 HOLogic.mk_prod (map_filter (fn (((((i, _), T), U), s), tname) =>
    1.36 -        if i mem is then SOME
    1.37 +        if member (op =) is i then SOME
    1.38            (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Free (tname, T))
    1.39          else NONE) (descr ~~ recTs ~~ rec_result_Ts ~~ rec_names ~~ tnames));
    1.40      val concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop @{const_name "op &"})
    1.41 @@ -131,7 +131,7 @@
    1.42      val ivs = rev (Term.add_vars (Logic.varify_global (Datatype_Prop.make_ind [descr] sorts)) []);
    1.43      val rvs = rev (Thm.fold_terms Term.add_vars thm' []);
    1.44      val ivs1 = map Var (filter_out (fn (_, T) =>  (* FIXME set (!??) *)
    1.45 -      tname_of (body_type T) mem [@{type_abbrev set}, @{type_name bool}]) ivs);
    1.46 +      member (op =) [@{type_abbrev set}, @{type_name bool}] (tname_of (body_type T))) ivs);
    1.47      val ivs2 = map (fn (ixn, _) => Var (ixn, the (AList.lookup (op =) rvs ixn))) ivs;
    1.48  
    1.49      val prf =