diff -r 34f1d2d81284 -r 006095137a81 src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Tue Mar 22 15:32:47 2011 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy	Tue Mar 22 16:15:50 2011 +0100
@@ -302,7 +302,7 @@
   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