src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
changeset 50170 8155e280f239
parent 49693 393d7242adaf
child 51380 cac8c9a636b6
     1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Nov 22 08:23:13 2012 +0100
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Nov 22 14:44:37 2012 +0100
     1.3 @@ -46,7 +46,10 @@
     1.4  val simp_attrs = @{attributes [simp]};
     1.5  val code_simp_attrs = Code.add_default_eqn_attrib :: simp_attrs;
     1.6  
     1.7 -fun split_list4 xs = (map #1 xs, map #2 xs, map #3 xs, map #4 xs);
     1.8 +fun split_list4 [] = ([], [], [], [])
     1.9 +  | split_list4 ((x1, x2, x3, x4) :: xs) =
    1.10 +    let val (xs1, xs2, xs3, xs4) = split_list4 xs;
    1.11 +    in (x1 :: xs1, x2 :: xs2, x3 :: xs3, x4 :: xs4) end;
    1.12  
    1.13  fun resort_tfree S (TFree (s, _)) = TFree (s, S);
    1.14  
    1.15 @@ -463,7 +466,7 @@
    1.16  
    1.17          fun wrap lthy =
    1.18            let
    1.19 -            fun exhaust_tac {context = ctxt, ...} =
    1.20 +            fun exhaust_tac {context = ctxt, prems = _} =
    1.21                let
    1.22                  val ctor_iff_dtor_thm =
    1.23                    let