diff -r c65614b556b2 -r 0b21b2beadb5 src/HOL/Word/Word.thy --- a/src/HOL/Word/Word.thy Thu Aug 06 17:51:37 2020 +0200 +++ b/src/HOL/Word/Word.thy Thu Aug 06 15:37:14 2020 +0000 @@ -415,11 +415,11 @@ begin lemma [transfer_rule]: - "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) of_bool of_bool" + "((=) ===> pcr_word) of_bool of_bool" by transfer_prover lemma [transfer_rule]: - "((=) ===> (pcr_word :: int \ 'a::len word \ bool)) numeral numeral" + "((=) ===> pcr_word) numeral numeral" by transfer_prover lemma [transfer_rule]: