# HG changeset patch
# User haftmann
# Date 1248540295 -7200
# Node ID 49db434c157fe4c7b0d1f2a4a0bd6b76b2b8db0c
# Parent  b330aa4d59cb40a784be9fd8e0c6d2b846320604
explicit is better than implicit

diff -r b330aa4d59cb -r 49db434c157f src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Sat Jul 25 18:44:54 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Sat Jul 25 18:44:55 2009 +0200
@@ -187,8 +187,12 @@
 lemma wf_empty [iff]: "wf({})"
   by (simp add: wf_def)
 
-lemmas wfP_empty [iff] =
-  wf_empty [to_pred bot_empty_eq2, simplified bot_fun_eq bot_bool_eq]
+lemma wfP_empty [iff]:
+  "wfP (\<lambda>x y. False)"
+proof -
+  have "wfP bot" by (fact wf_empty [to_pred bot_empty_eq2])
+  then show ?thesis by (simp add: bot_fun_eq bot_bool_eq)
+qed
 
 lemma wf_Int1: "wf r ==> wf (r Int r')"
   apply (erule wf_subset)