--- a/src/HOL/Library/Old_Recdef.thy Mon Mar 17 11:30:39 2025 +0100 +++ b/src/HOL/Library/Old_Recdef.thy Mon Mar 17 16:29:48 2025 +0100 @@ -82,6 +82,6 @@ wf_measures wf_pred_nat wf_same_fst - wf_empty + wf_on_bot end