src/HOL/Isar_Examples/Hoare.thy

 proof -
   have "|- {s. id s : P} SKIP P" by (rule basic)
   then show ?thesis by simp
 qed
 
-lemma assign: "|- P [\<acute>a/\<acute>x] \<acute>x := \<acute>a P"
+lemma assign: "|- P [\<acute>a/\<acute>x::'a] \<acute>x := \<acute>a P"
   by (rule basic)
 
 text {* Note that above formulation of assignment corresponds to our
   preferred way to model state spaces, using (extensible) record types
   in HOL \cite{Naraschewski-Wenzel:1998:HOOL}.  For any record field