# HG changeset patch
# User kuncar
# Date 1337346488 -7200
# Node ID 22e00179564185f83fdf8a16e5839b1ed8a89d94
# Parent  4ef90b51641e6c84b4f1a51525934c1139f196e3
don't generate code in Word because it breaks the current code setup

diff -r 4ef90b51641e -r 22e001795641 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Thu May 17 13:36:23 2012 +0200
+++ b/src/HOL/Word/Word.thy	Fri May 18 15:08:08 2012 +0200
@@ -245,7 +245,7 @@
   "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
   by (simp add: reflp_def)
 
-setup_lifting Quotient_word reflp_word
+setup_lifting(no_code) Quotient_word reflp_word
 
 text {* TODO: The next lemma could be generated automatically. *}