src/HOL/Tools/inductive_realizer.ML
changeset 19473 d87a8838afa4
parent 19046 bc5c6c9b114e
child 19510 29fc4e5a638c
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Wed Apr 26 20:34:11 2006 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Wed Apr 26 22:38:05 2006 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4        else NONE) rss;
     1.5      val fs = List.concat (snd (foldl_map (fn (intrs, (prems, dummy)) =>
     1.6        let
     1.7 -        val (intrs1, intrs2) = splitAt (length prems, intrs);
     1.8 +        val (intrs1, intrs2) = chop (length prems) intrs;
     1.9          val fs = map (fn (rule, intr) =>
    1.10            fun_of_prem thy rsets vs params rule intr) (prems ~~ intrs1)
    1.11        in (intrs2, if dummy then Const ("arbitrary",
    1.12 @@ -330,7 +330,7 @@
    1.13        if s mem rsets then
    1.14          let
    1.15            val (d :: dummies') = dummies;
    1.16 -          val (recs1, recs2) = splitAt (length rs, if d then tl recs else recs)
    1.17 +          val (recs1, recs2) = chop (length rs) (if d then tl recs else recs)
    1.18          in ((recs2, dummies'), map (head_of o hd o rev o snd o strip_comb o
    1.19            fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) recs1)
    1.20          end