# HG changeset patch
# User blanchet
# Date 1366730144 -7200
# Node ID a06a3c777addb0a439df42789804bc1228dec093
# Parent  0468af6546ff2e81fdb02b13dfc1ca0507c7bf1c
simplify "Inl () = Inr ()" as well (not entirely clear why this is necessary)

diff -r 0468af6546ff -r a06a3c777add src/HOL/BNF/BNF_FP.thy
--- a/src/HOL/BNF/BNF_FP.thy	Tue Apr 23 17:13:14 2013 +0200
+++ b/src/HOL/BNF/BNF_FP.thy	Tue Apr 23 17:15:44 2013 +0200
@@ -116,6 +116,9 @@
 "\<Union>{y. \<exists>x\<in>A. y = {x}} = A"
 by blast+
 
+lemma Inl_Inr_False: "(Inl x = Inr y) = False"
+by simp
+
 lemma prod_set_simps:
 "fsts (x, y) = {x}"
 "snds (x, y) = {y}"
diff -r 0468af6546ff -r a06a3c777add src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:13:14 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue Apr 23 17:15:44 2013 +0200
@@ -550,8 +550,8 @@
 
             fun mk_rel_thm postproc ctr_defs' cxIn cyIn =
               fold_thms lthy ctr_defs'
-                 (unfold_thms lthy (pre_rel_def :: (if lfp then [] else [dtor_ctor]) @
-                      sum_prod_thms_rel)
+                 (unfold_thms lthy (@{thm Inl_Inr_False} :: pre_rel_def ::
+                      (if lfp then [] else [dtor_ctor]) @ sum_prod_thms_rel)
                     (cterm_instantiate_pos (nones @ [SOME cxIn, SOME cyIn]) fp_rel_thm))
               |> postproc
               |> singleton (Proof_Context.export names_lthy no_defs_lthy);