--- 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