--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 20:54:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML Wed Sep 05 23:59:44 2012 +0200
@@ -99,10 +99,12 @@
val raw_disc_binders' = pad_list no_binder n raw_disc_binders;
- fun can_rely_on_disc k =
+ fun can_really_rely_on_disc k =
not (Binding.eq_name (nth raw_disc_binders' (k - 1), no_binder)) orelse nth ms (k - 1) = 0;
+ fun can_rely_on_disc k =
+ can_really_rely_on_disc k orelse (k = 1 andalso not (can_really_rely_on_disc 2));
fun can_omit_disc_binder k m =
- n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k))
+ n = 1 orelse m = 0 orelse (n = 2 andalso can_rely_on_disc (3 - k));
val fallback_disc_binder = Binding.name o prefix is_N o Long_Name.base_name o name_of_ctr;
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Wed Sep 05 20:54:40 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML Wed Sep 05 23:59:44 2012 +0200
@@ -45,10 +45,11 @@
EVERY' [rtac iffI, rtac exhaust', REPEAT_DETERM_N m o rtac exI, atac, rtac refl] 1;
fun mk_alternate_disc_def_tac ctxt k other_disc_def distinct exhaust' =
- EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, hyp_subst_tac,
- SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, rtac distinct,
- rtac exhaust'] @
- (([etac notE, atac], [REPEAT_DETERM o rtac exI, atac]) |> k = 1 ? swap |> op @)) 1;
+ EVERY' ([subst_tac ctxt [other_disc_def], rtac @{thm iffI_np}, REPEAT_DETERM o etac exE,
+ hyp_subst_tac, SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI,
+ rtac distinct, rtac exhaust'] @
+ (([etac notE, REPEAT_DETERM o rtac exI, atac], [REPEAT_DETERM o rtac exI, atac])
+ |> k = 1 ? swap |> op @)) 1;
fun mk_half_disc_exclude_tac m discD disc'_thm =
(dtac discD THEN'