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