src/HOL/BNF/Tools/bnf_wrap.ML

--- a/src/HOL/BNF/Tools/bnf_wrap.ML	Sun Sep 30 12:08:16 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_wrap.ML	Sun Sep 30 22:02:34 2012 +0200
@@ -80,7 +80,7 @@
     val xsss =
       map2 (map2 append) (Library.chop_groups n half_xss)
         (transpose (Library.chop_groups n other_half_xss))
-    val xs = interleave (flat half_xss) (flat other_half_xss);
+    val xs = splice (flat half_xss) (flat other_half_xss);
   in (xs, xsss) end;
 
 fun mk_undefined T = Const (@{const_name undefined}, T);