src/HOL/Tools/inductive_realizer.ML
changeset 31458 b1cf26f2919b
parent 31177 c39994cb152a
child 31668 a616e56a5ec8
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Thu Jun 04 16:11:03 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Thu Jun 04 16:11:04 2009 +0200
     1.3 @@ -315,16 +315,16 @@
     1.4      fun get f = (these oo Option.map) f;
     1.5      val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o
     1.6        HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) (get #rec_thms dt_info));
     1.7 -    val (_, constrss) = Library.foldl_map (fn ((recs, dummies), (s, rs)) =>
     1.8 -      if s mem rsets then
     1.9 +    val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) =>
    1.10 +      if member (op =) rsets s then
    1.11          let
    1.12            val (d :: dummies') = dummies;
    1.13            val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
    1.14 -        in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
    1.15 -          fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
    1.16 +        in (map (head_of o hd o rev o snd o strip_comb o fst o
    1.17 +          HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1, (recs2, dummies'))
    1.18          end
    1.19 -      else ((recs, dummies), replicate (length rs) Extraction.nullt))
    1.20 -        ((get #rec_thms dt_info, dummies), rss);
    1.21 +      else (replicate (length rs) Extraction.nullt, (recs, dummies)))
    1.22 +        rss (get #rec_thms dt_info, dummies);
    1.23      val rintrs = map (fn (intr, c) => Envir.eta_contract
    1.24        (Extraction.realizes_of thy2 vs
    1.25          (if c = Extraction.nullt then c else list_comb (c, map Var (rev
    1.26 @@ -360,7 +360,7 @@
    1.27  
    1.28      (** realizer for induction rule **)
    1.29  
    1.30 -    val Ps = List.mapPartial (fn _ $ M $ P => if pred_of M mem rsets then
    1.31 +    val Ps = map_filter (fn _ $ M $ P => if pred_of M mem rsets then
    1.32        SOME (fst (fst (dest_Var (head_of P)))) else NONE)
    1.33          (HOLogic.dest_conj (HOLogic.dest_Trueprop (concl_of raw_induct)));
    1.34