src/HOL/Tools/hologic.ML
changeset 36692 54b64d4ad524
parent 35625 9c818cab0dd0
child 37145 01aa36932739
     1.1 --- a/src/HOL/Tools/hologic.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/hologic.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -356,7 +356,7 @@
     1.4  fun mk_ptupleT ps =
     1.5    let
     1.6      fun mk p Ts =
     1.7 -      if p mem ps then
     1.8 +      if member (op =) ps p then
     1.9          let
    1.10            val (T, Ts') = mk (1::p) Ts;
    1.11            val (U, Ts'') = mk (2::p) Ts'
    1.12 @@ -366,7 +366,7 @@
    1.13  
    1.14  fun strip_ptupleT ps =
    1.15    let
    1.16 -    fun factors p T = if p mem ps then (case T of
    1.17 +    fun factors p T = if member (op =) ps p then (case T of
    1.18          Type ("*", [T1, T2]) =>
    1.19            factors (1::p) T1 @ factors (2::p) T2
    1.20        | _ => ptuple_err "strip_ptupleT") else [T]
    1.21 @@ -382,7 +382,7 @@
    1.22  fun mk_ptuple ps =
    1.23    let
    1.24      fun mk p T ts =
    1.25 -      if p mem ps then (case T of
    1.26 +      if member (op =) ps p then (case T of
    1.27            Type ("*", [T1, T2]) =>
    1.28              let
    1.29                val (t, ts') = mk (1::p) T1 ts;
    1.30 @@ -394,7 +394,7 @@
    1.31  
    1.32  fun strip_ptuple ps =
    1.33    let
    1.34 -    fun dest p t = if p mem ps then (case t of
    1.35 +    fun dest p t = if member (op =) ps p then (case t of
    1.36          Const ("Pair", _) $ t $ u =>
    1.37            dest (1::p) t @ dest (2::p) u
    1.38        | _ => ptuple_err "strip_ptuple") else [t]
    1.39 @@ -413,7 +413,7 @@
    1.40  fun mk_psplits ps T T3 u =
    1.41    let
    1.42      fun ap ((p, T) :: pTs) =
    1.43 -          if p mem ps then (case T of
    1.44 +          if member (op =) ps p then (case T of
    1.45                Type ("*", [T1, T2]) =>
    1.46                  split_const (T1, T2, map snd pTs ---> T3) $
    1.47                    ap ((1::p, T1) :: (2::p, T2) :: pTs)