--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Aug 10 14:31:06 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sun Aug 10 14:34:43 2014 +0200
@@ -1336,7 +1336,14 @@
val tacss = [exhaust_tac] :: inject_tacss @ half_distinct_tacss;
- val sel_default_eqs = map (prepare_term lthy) raw_sel_default_eqs;
+ val sel_Tss = map (map (curry (op -->) fpT)) ctr_Tss;
+ val sel_bTs =
+ flat sel_bindingss ~~ flat sel_Tss
+ |> filter_out (Binding.is_empty o fst)
+ |> distinct (Binding.eq_name o pairself fst);
+ val sel_default_lthy = fake_local_theory_for_sel_defaults sel_bTs lthy;
+
+ val sel_default_eqs = map (prepare_term sel_default_lthy) raw_sel_default_eqs;
fun ctr_spec_of disc_b ctr0 sel_bs = ((disc_b, ctr0), sel_bs);
val ctr_specs = map3 ctr_spec_of disc_bindings ctrs0 sel_bindingss;
@@ -1570,7 +1577,8 @@
val thm = Goal.prove_sorry lthy [] [] goal
(fn {context = ctxt, prems = _} =>
mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
- injects rel_inject_thms distincts rel_distinct_thms)
+ injects rel_inject_thms distincts rel_distinct_thms
+ (map rel_eq_of_bnf live_nesting_bnfs))
|> singleton (Proof_Context.export names_lthy lthy)
|> Thm.close_derivation;