# HG changeset patch
# User bulwahn
# Date 1342102953 -7200
# Node ID 4410a709913ca8b06c79ad5e7f3a9b89b42debb1
# Parent  e98c3d50ae627690011c1f5cc26a473e73623761
a first guess to avoid the Codegenerator_Test to loop infinitely

diff -r e98c3d50ae62 -r 4410a709913c 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
 
diff -r e98c3d50ae62 -r 4410a709913c src/HOL/Relation.thy
--- a/src/HOL/Relation.thy	Thu Jul 12 21:46:11 2012 +1000
+++ b/src/HOL/Relation.thy	Thu Jul 12 16:22:33 2012 +0200
@@ -427,7 +427,7 @@
 
 definition Id :: "'a rel"
 where
-  "Id = {p. \<exists>x. p = (x, x)}"
+  [code del]: "Id = {p. \<exists>x. p = (x, x)}"
 
 lemma IdI [intro]: "(a, a) : Id"
   by (simp add: Id_def)