diff -r 57752a91eec4 -r 117ba6cbe414 src/HOL/Library/Bit.thy --- 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)"