src/FOLP/simp.ML
changeset 36692 54b64d4ad524
parent 36603 d5d6111761a6
child 36945 9bec62c10714
     1.1 --- a/src/FOLP/simp.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/FOLP/simp.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -98,7 +98,7 @@
     1.4  in var(lhs_of_eq i thm) end;
     1.5  
     1.6  fun contains_op opns =
     1.7 -    let fun contains(Const(s,_)) = s mem opns |
     1.8 +    let fun contains(Const(s,_)) = member (op =) opns s |
     1.9              contains(s$t) = contains s orelse contains t |
    1.10              contains(Abs(_,_,t)) = contains t |
    1.11              contains _ = false;
    1.12 @@ -117,7 +117,7 @@
    1.13    in map norm normE_thms end;
    1.14  
    1.15  fun lhs_is_NORM(thm,i) = case lhs_of_eq i thm of
    1.16 -        Const(s,_)$_ => s mem norms | _ => false;
    1.17 +        Const(s,_)$_ => member (op =) norms s | _ => false;
    1.18  
    1.19  val refl_tac = resolve_tac refl_thms;
    1.20  
    1.21 @@ -203,7 +203,7 @@
    1.22      val refl1_tac = refl_tac 1
    1.23      fun norm_step_tac st = st |>
    1.24           (case head_of(rhs_of_eq 1 st) of
    1.25 -            Var(ixn,_) => if ixn mem hvs then refl1_tac
    1.26 +            Var(ixn,_) => if member (op =) hvs ixn then refl1_tac
    1.27                            else resolve_tac normI_thms 1 ORELSE refl1_tac
    1.28            | Const _ => resolve_tac normI_thms 1 ORELSE
    1.29                         resolve_tac congs 1 ORELSE refl1_tac