diff -r 762eb0dacaa6 -r c201a1fe0a81 src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Wed Apr 18 23:13:11 2012 +0200
+++ b/src/HOL/Word/Word.thy	Wed Apr 18 23:57:44 2012 +0200
@@ -243,9 +243,7 @@
   "reflp (\<lambda>x y. bintrunc (len_of TYPE('a::len0)) x = bintrunc (len_of TYPE('a)) y)"
   by (simp add: reflp_def)
 
-local_setup {*
-  Lifting_Setup.setup_by_quotient @{thm Quotient_word} (SOME @{thm reflp_word})
-*}
+setup_lifting Quotient_word reflp_word
 
 text {* TODO: The next lemma could be generated automatically. *}