diff -r 56e83c57f953 -r c2f30ba4bb98 src/HOL/IMP/Denotational.thy
--- a/src/HOL/IMP/Denotational.thy	Thu Jun 20 17:43:36 2013 +0200
+++ b/src/HOL/IMP/Denotational.thy	Fri Jun 21 09:00:26 2013 +0200
@@ -71,10 +71,10 @@
 lemma chain_total: "chain S \<Longrightarrow> S i \<le> S j \<or> S j \<le> S i"
 by (metis chain_def le_cases lift_Suc_mono_le)
 
-definition cont :: "('a set \<Rightarrow> 'a set) \<Rightarrow> bool" where
+definition cont :: "('a set \<Rightarrow> 'b set) \<Rightarrow> bool" where
 "cont f = (\<forall>S. chain S \<longrightarrow> f(UN n. S n) = (UN n. f(S n)))"
 
-lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'a set"
+lemma mono_if_cont: fixes f :: "'a set \<Rightarrow> 'b set"
   assumes "cont f" shows "mono f"
 proof
   fix a b :: "'a set" assume "a \<subseteq> b"