src/ZF/Tools/inductive_package.ML
changeset 36692 54b64d4ad524
parent 36610 bafd82950e24
child 36954 ef698bd61057
     1.1 --- a/src/ZF/Tools/inductive_package.ML	Wed May 05 09:24:42 2010 +0200
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Wed May 05 18:25:34 2010 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4    local (*Checking the introduction rules*)
     1.5      val intr_sets = map (#2 o rule_concl_msg thy) intr_tms;
     1.6      fun intr_ok set =
     1.7 -        case head_of set of Const(a,recT) => a mem rec_names | _ => false;
     1.8 +        case head_of set of Const(a,recT) => member (op =) rec_names a | _ => false;
     1.9    in
    1.10      val dummy =  assert_all intr_ok intr_sets
    1.11         (fn t => "Conclusion of rule does not name a recursive set: " ^