# HG changeset patch
# User blanchet
# Date 1346882384 -7200
# Node ID 41790d616f639bad7181aa4abfb1d06fa7c7a853
# Parent  fa01a202399c2a071ac19e9dd031ea24e2d094c7
by default, only generate one discriminator for a two-value datatype

diff -r fa01a202399c -r 41790d616f63 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- 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;
 
diff -r fa01a202399c -r 41790d616f63 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- 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'