--- a/thys2/Recs.thy	Thu Jan 10 13:00:04 2019 +0000
+++ b/thys2/Recs.thy	Thu Jan 10 13:18:07 2019 +0000
@@ -533,11 +533,7 @@
 
 lemma Quo_div: 
   shows "Quo x y = y div x"
-apply(case_tac "x = 0")
-apply(simp add: Quo0)
-apply(subst split_div_lemma[symmetric])
-apply(auto intro: Quo1 Quo4)
-done
+by (metis Quo0 Quo1 Quo4 div_by_0 div_nat_eqI mult_Suc_right neq0_conv)
 
 lemma Quo_rec_quo:
   shows "rec_eval rec_quo [y, x] = Quo x y"