src/Pure/Proof/extraction.ML
changeset 20664 ffbc5a57191a
parent 20548 8ef25fe585a8
child 20854 f9cf9e62d11c
     1.1 --- a/src/Pure/Proof/extraction.ML	Thu Sep 21 19:04:12 2006 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Thu Sep 21 19:04:20 2006 +0200
     1.3 @@ -54,10 +54,10 @@
     1.4  fun typeof_proc defaultS vs (Const ("typeof", _) $ u) =
     1.5        SOME (mk_typ (case strip_comb u of
     1.6            (Var ((a, i), _), _) =>
     1.7 -            if a mem vs then TFree ("'" ^ a ^ ":" ^ string_of_int i, defaultS)
     1.8 +            if member (op =) vs a then TFree ("'" ^ a ^ ":" ^ string_of_int i, defaultS)
     1.9              else nullT
    1.10          | (Free (a, _), _) =>
    1.11 -            if a mem vs then TFree ("'" ^ a, defaultS) else nullT
    1.12 +            if member (op =) vs a then TFree ("'" ^ a, defaultS) else nullT
    1.13          | _ => nullT))
    1.14    | typeof_proc _ _ _ = NONE;
    1.15  
    1.16 @@ -147,7 +147,7 @@
    1.17  
    1.18  fun relevant_vars types prop = foldr (fn
    1.19        (Var ((a, i), T), vs) => (case strip_type T of
    1.20 -        (_, Type (s, _)) => if s mem types then a :: vs else vs
    1.21 +        (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
    1.22        | _ => vs)
    1.23      | (_, vs) => vs) [] (vars_of prop);
    1.24  
    1.25 @@ -320,7 +320,7 @@
    1.26          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
    1.27        val vars = vars_of prop;
    1.28        val vars' = filter_out (fn v =>
    1.29 -        tname_of (body_type (fastype_of v)) mem rtypes) vars;
    1.30 +        member (op =) rtypes (tname_of (body_type (fastype_of v)))) vars;
    1.31        val T = etype_of thy' vs [] prop;
    1.32        val (T', thw) = Type.freeze_thaw_type
    1.33          (if T = nullT then nullT else map fastype_of vars' ---> T);
    1.34 @@ -474,7 +474,7 @@
    1.35          val n = Int.min (length vars, length ts);
    1.36  
    1.37          fun add_args ((Var ((a, i), _), t), (vs', tye)) =
    1.38 -          if a mem rvs then
    1.39 +          if member (op =) rvs a then
    1.40              let val T = etype_of thy' vs Ts t
    1.41              in if T = nullT then (vs', tye)
    1.42                 else (a :: vs', (("'" ^ a, i), T) :: tye)
    1.43 @@ -483,7 +483,7 @@
    1.44  
    1.45        in foldr add_args ([], []) (Library.take (n, vars) ~~ Library.take (n, ts)) end;
    1.46  
    1.47 -    fun find vs = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    1.48 +    fun find (vs: string list) = Option.map snd o find_first (curry (gen_eq_set (op =)) vs o fst);
    1.49      fun find' s = map snd o List.filter (equal s o fst)
    1.50  
    1.51      fun app_rlz_rews Ts vs t = strip_abs (length Ts) (freeze_thaw
    1.52 @@ -523,9 +523,9 @@
    1.53            let
    1.54              val (Us, T) = strip_type (fastype_of1 (Ts, t));
    1.55              val (defs', corr_prf) = corr d defs vs (t :: ts) Ts hs prf prf'
    1.56 -              (if tname_of T mem rtypes then t'
    1.57 +              (if member (op =) rtypes (tname_of T) then t'
    1.58                 else (case t' of SOME (u $ _) => SOME u | _ => NONE));
    1.59 -            val u = if not (tname_of T mem rtypes) then t else
    1.60 +            val u = if not (member (op =) rtypes (tname_of T)) then t else
    1.61                let
    1.62                  val eT = etype_of thy' vs Ts t;
    1.63                  val (r, Us') = if eT = nullT then (nullt, Us) else
    1.64 @@ -628,7 +628,7 @@
    1.65        | extr d defs vs ts Ts hs (prf % SOME t) =
    1.66            let val (defs', u) = extr d defs vs (t :: ts) Ts hs prf
    1.67            in (defs',
    1.68 -            if tname_of (body_type (fastype_of1 (Ts, t))) mem rtypes then u
    1.69 +            if member (op =) rtypes (tname_of (body_type (fastype_of1 (Ts, t)))) then u
    1.70              else u $ t)
    1.71            end
    1.72  
    1.73 @@ -661,8 +661,8 @@
    1.74                        corr (d + 1) defs' vs' [] [] [] prf' prf' (SOME t);
    1.75  
    1.76                      val nt = Envir.beta_norm t;
    1.77 -                    val args = filter_out (fn v => tname_of (body_type
    1.78 -                      (fastype_of v)) mem rtypes) (vfs_of prop);
    1.79 +                    val args = filter_out (fn v => member (op =) rtypes
    1.80 +                      (tname_of (body_type (fastype_of v)))) (vfs_of prop);
    1.81                      val args' = List.filter (fn v => Logic.occs (v, nt)) args;
    1.82                      val t' = mkabs nt args';
    1.83                      val T = fastype_of t';