
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 \<Rightarrow> 'a::len word \<Rightarrow> bool)) of_bool of_bool"
+  "((=) ===> pcr_word) of_bool of_bool"
   by transfer_prover
 
 lemma [transfer_rule]:
-  "((=) ===> (pcr_word :: int \<Rightarrow> 'a::len word \<Rightarrow> bool)) numeral numeral"
+  "((=) ===> pcr_word) numeral numeral"
   by transfer_prover
 
 lemma [transfer_rule]:




