1.1 --- a/src/ZF/Tools/inductive_package.ML	Fri Feb 11 18:51:00 2005 +0100
     1.2 +++ b/src/ZF/Tools/inductive_package.ML	Sun Feb 13 17:15:14 2005 +0100
     1.3 @@ -301,8 +301,8 @@
     1.4       fun add_induct_prem ind_alist (prem as Const("Trueprop",_) $
     1.5                        (Const("op :",_)$t$X), iprems) =
     1.6            (case gen_assoc (op aconv) (ind_alist, X) of
     1.7 -               Some pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
     1.8 -             | None => (*possibly membership in M(rec_tm), for M monotone*)
     1.9 +               SOME pred => prem :: FOLogic.mk_Trueprop (pred $ t) :: iprems
    1.10 +             | NONE => (*possibly membership in M(rec_tm), for M monotone*)
    1.11                   let fun mk_sb (rec_tm,pred) =
    1.12                               (rec_tm, Ind_Syntax.Collect_const$rec_tm$pred)
    1.13                   in  subst_free (map mk_sb ind_alist) prem :: iprems  end)
    1.14 @@ -314,7 +314,7 @@
    1.15             val iprems = foldr (add_induct_prem ind_alist)
    1.16                                (Logic.strip_imp_prems intr,[])
    1.17             val (t,X) = Ind_Syntax.rule_concl intr
    1.18 -           val (Some pred) = gen_assoc (op aconv) (ind_alist, X)
    1.19 +           val (SOME pred) = gen_assoc (op aconv) (ind_alist, X)
    1.20             val concl = FOLogic.mk_Trueprop (pred $ t)
    1.21         in list_all_free (quantfrees, Logic.list_implies (iprems,concl)) end
    1.22         handle Bind => error"Recursion term not found in conclusion";