--- a/thys/Rec_Def.thy	Wed Jan 14 09:08:51 2015 +0000
+++ b/thys/Rec_Def.thy	Wed Dec 19 16:10:58 2018 +0100
@@ -28,7 +28,7 @@
 
 termination
 apply(relation "measures [\<lambda> (r, xs). size r, (\<lambda> (r, xs). last xs)]")
-apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 list_size_estimation')
+apply(auto simp add: less_Suc_eq_le intro: trans_le_add2 size_list_estimation'[THEN trans_le_add1])
 done
 
 inductive terminate :: "recf \<Rightarrow> nat list \<Rightarrow> bool"