diff -r ae634fad947e -r 18b41bba42b5 src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Thu Jan 28 11:48:43 2010 +0100
+++ b/src/HOL/ex/Binary.thy	Thu Jan 28 11:48:49 2010 +0100
@@ -27,8 +27,8 @@
     | dest_bit (Const (@{const_name True}, _)) = 1
     | dest_bit t = raise TERM ("dest_bit", [t]);
 
-  fun dest_binary (Const (@{const_name HOL.zero}, Type (@{type_name nat}, _))) = 0
-    | dest_binary (Const (@{const_name HOL.one}, Type (@{type_name nat}, _))) = 1
+  fun dest_binary (Const (@{const_name Algebras.zero}, Type (@{type_name nat}, _))) = 0
+    | dest_binary (Const (@{const_name Algebras.one}, Type (@{type_name nat}, _))) = 1
     | dest_binary (Const (@{const_name bit}, _) $ bs $ b) = 2 * dest_binary bs + dest_bit b
     | dest_binary t = raise TERM ("dest_binary", [t]);