--- a/src/HOL/Inductive.thy Fri Nov 30 16:23:52 2007 +0100
+++ b/src/HOL/Inductive.thy Fri Nov 30 20:13:03 2007 +0100
@@ -290,8 +290,10 @@
val def_gfp_unfold = @{thm def_gfp_unfold}
val def_lfp_induct = @{thm def_lfp_induct}
val def_coinduct = @{thm def_coinduct}
-val inf_bool_eq = @{thm inf_bool_eq}
-val inf_fun_eq = @{thm inf_fun_eq}
+val inf_bool_eq = @{thm inf_bool_eq} RS @{thm eq_reflection}
+val inf_fun_eq = @{thm inf_fun_eq} RS @{thm eq_reflection}
+val sup_bool_eq = @{thm sup_bool_eq} RS @{thm eq_reflection}
+val sup_fun_eq = @{thm sup_fun_eq} RS @{thm eq_reflection}
val le_boolI = @{thm le_boolI}
val le_boolI' = @{thm le_boolI'}
val le_funI = @{thm le_funI}
@@ -299,8 +301,8 @@
val le_funE = @{thm le_funE}
val le_boolD = @{thm le_boolD}
val le_funD = @{thm le_funD}
-val le_bool_def = @{thm le_bool_def}
-val le_fun_def = @{thm le_fun_def}
+val le_bool_def = @{thm le_bool_def} RS @{thm eq_reflection}
+val le_fun_def = @{thm le_fun_def} RS @{thm eq_reflection}
*}
use "Tools/inductive_package.ML"