--- a/src/HOL/Recdef.thy Wed Jul 11 11:07:57 2007 +0200 +++ b/src/HOL/Recdef.thy Wed Jul 11 11:09:15 2007 +0200 @@ -75,7 +75,5 @@ wf_pred_nat wf_same_fst wf_empty - wf_implies_wfP - wfP_implies_wf end