src/HOL/Tools/inductive.ML
changeset 36692 54b64d4ad524
parent 36642 084470c3cea2
child 36954 ef698bd61057
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -288,7 +288,7 @@
     1.4            then err bad_ind_occ else ();
     1.5  
     1.6      fun check_prem' prem t =
     1.7 -      if head_of t mem cs then
     1.8 +      if member (op =) cs (head_of t) then
     1.9          check_ind (err_in_prem ctxt err_name rule prem) t
    1.10        else (case t of
    1.11            Abs (_, _, t) => check_prem' prem t
    1.12 @@ -301,7 +301,7 @@
    1.13    in
    1.14      (case concl of
    1.15         Const (@{const_name Trueprop}, _) $ t =>
    1.16 -         if head_of t mem cs then
    1.17 +         if member (op =) cs (head_of t) then
    1.18             (check_ind (err_in_rule ctxt err_name rule') t;
    1.19              List.app check_prem (prems ~~ aprems))
    1.20           else err_in_rule ctxt err_name rule' bad_concl