src/HOL/Quickcheck_Narrowing.thy

--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jul 12 21:46:11 2012 +1000
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jul 12 16:22:33 2012 +0200
@@ -138,10 +138,6 @@
   [code del]: "div_mod n m = (n div m, n mod m)"
 
 lemma [code]:
-  "div_mod n m = (if m = 0 then (0, n) else (n div m, n mod m))"
-  unfolding div_mod_def by auto
-
-lemma [code]:
   "n div m = fst (div_mod n m)"
   unfolding div_mod_def by simp