# HG changeset patch
# User blanchet
# Date 1380196268 -7200
# Node ID 0fc622be018571a1859437396d10d66ad839a671
# Parent  bf74357f91f86286e18c0d14309e7fe3dde86ba7
use new "sel_split(_asm)" to avoid giving rise to quantifiers, which would in turn require relying on injectivity

diff -r bf74357f91f8 -r 0fc622be0185 src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 13:42:14 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar.ML	Thu Sep 26 13:51:08 2013 +0200
@@ -800,9 +800,9 @@
               |> HOLogic.mk_Trueprop o HOLogic.mk_eq
               |> curry Logic.list_implies (map HOLogic.mk_Trueprop prems)
               |> curry Logic.list_all (map dest_Free fun_args);
-            val (distincts, _, _, splits, split_asms) = case_thms_of_term lthy [] rhs_term;
+            val (distincts, _, _, sel_splits, sel_split_asms) = case_thms_of_term lthy [] rhs_term;
           in
-            mk_primcorec_sel_tac lthy def_thms distincts splits split_asms nested_maps
+            mk_primcorec_sel_tac lthy def_thms distincts sel_splits sel_split_asms nested_maps
               nested_map_idents nested_map_comps sel_corec k m exclsss
             |> K |> Goal.prove lthy [] [] t
             |> pair sel
diff -r bf74357f91f8 -r 0fc622be0185 src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 13:42:14 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_rec_sugar_util.ML	Thu Sep 26 13:51:08 2013 +0200
@@ -398,7 +398,7 @@
     val ctr_sugars = map (the o ctr_sugar_of ctxt) caseT_names;
   in
     (maps #distincts ctr_sugars, maps #discIs ctr_sugars, maps #collapses ctr_sugars,
-     map #split ctr_sugars, map #split_asm ctr_sugars)
+     maps #sel_splits ctr_sugars, maps #sel_split_asms ctr_sugars)
   end;
 
 fun indexed xs h = let val h' = h + length xs in (h upto h' - 1, h') end;