--- a/src/HOL/Library/Bit.thy Thu Sep 11 18:54:36 2014 +0200
+++ b/src/HOL/Library/Bit.thy Thu Sep 11 18:54:36 2014 +0200
@@ -27,7 +27,7 @@
end
-rep_datatype "0::bit" "1::bit"
+old_rep_datatype "0::bit" "1::bit"
proof -
fix P and x :: bit
assume "P (0::bit)" and "P (1::bit)"