# HG changeset patch
# User blanchet
# Date 1457681997 -3600
# Node ID 75452e3eda14637c99281a073c01a68b9ae945fa
# Parent  adffc55a682d916cf32b7854d7fd928cca3f7b9e
generate theorems like 'bool.split_sel'

diff -r adffc55a682d -r 75452e3eda14 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Thu Mar 10 22:49:24 2016 +0100
+++ b/src/HOL/Product_Type.thy	Fri Mar 11 08:39:57 2016 +0100
@@ -12,7 +12,7 @@
 
 subsection \<open>@{typ bool} is a datatype\<close>
 
-free_constructors case_bool for True | False
+free_constructors (discs_sels) case_bool for True | False
   by auto
 
 text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>