# HG changeset patch
# User wenzelm
# Date 1353601566 -3600
# Node ID d655dda100c53b8bbb0b849e000a07edb6ba09b1
# Parent  8155e280f239e51c4952b9458c4baaea478d346d# Parent  071902349e3ef631951e5185a4cb50fe9996f3b5
merged

diff -r 071902349e3e -r d655dda100c5 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Nov 22 17:11:26 2012 +0100
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Nov 22 17:26:06 2012 +0100
@@ -46,7 +46,10 @@
 val simp_attrs = @{attributes [simp]};
 val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
 
-fun split_list4 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs);
+fun split_list4 [] = ([], [], [], [])
+  | split_list4 ((x1, x2, x3, x4) :: xs) =
+    let val (xs1, xs2, xs3, xs4) = split_list4 xs;
+    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
 
 fun resort_tfree S (TFree (s, _)) = TFree (s, S);
 
@@ -463,7 +466,7 @@
 
         fun wrap lthy =
           let
-            fun exhaust_tac {context = ctxt, ...} =
+            fun exhaust_tac {context = ctxt, prems = _} =
               let
                 val ctor_iff_dtor_thm =
                   let