src/HOL/Tools/inductive_realizer.ML
changeset 31986 a68f88d264f7
parent 31784 bd3486c57ba3
child 32091 30e2ffbba718
child 32125 10e1a6ea8df9
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Jul 10 07:59:25 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Jul 10 07:59:27 2009 +0200
     1.3 @@ -204,9 +204,9 @@
     1.4  fun indrule_realizer thy induct raw_induct rsets params vs rec_names rss intrs dummies =
     1.5    let
     1.6      val concls = HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct));
     1.7 -    val premss = List.mapPartial (fn (s, rs) => if s mem rsets then
     1.8 -      SOME (rs, map (fn (_, r) => List.nth (prems_of raw_induct,
     1.9 -        find_index_eq (prop_of r) (map prop_of intrs))) rs) else NONE) rss;
    1.10 +    val premss = map_filter (fn (s, rs) => if member (op =) rsets s then
    1.11 +      SOME (rs, map (fn (_, r) => nth (prems_of raw_induct)
    1.12 +        (find_index (fn prp => prp = prop_of r) (map prop_of intrs))) rs) else NONE) rss;
    1.13      val fs = maps (fn ((intrs, prems), dummy) =>
    1.14        let
    1.15          val fs = map (fn (rule, (ivs, intr)) =>