1.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 13:42:14 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 13:51:08 2013 +0200
     1.3 @@ -800,9 +800,9 @@
     1.4                |> HOLogic.mk_Trueprop o HOLogic.mk_eq
     1.5                |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
     1.6                |> curry Logic.list_all (map dest_Free fun_args);
     1.7 -            val (distincts, _, _, splits, split_asms) = case_thms_of_term lthy [] rhs_term;
     1.8 +            val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
     1.9            in
    1.10 -            mk_primcorec_sel_tac lthy def_thms distincts splits split_asms nested_maps
    1.11 +            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
    1.12                nested_map_idents nested_map_comps sel_corec k m exclsss
    1.13              |> K |> Goal.prove lthy [] [] t
    1.14              |> pair sel

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 13:42:14 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 13:51:08 2013 +0200
     2.3 @@ -398,7 +398,7 @@
     2.4      val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
     2.5    in
     2.6      (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #collapses ctr_sugars,
     2.7 -     map #split ctr_sugars, map #split_asm ctr_sugars)
     2.8 +     maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
     2.9    end;
    2.10  
    2.11  fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;