--- a/src/HOL/IMP/Collecting.thy Wed Jan 04 12:09:53 2012 +0100
+++ b/src/HOL/IMP/Collecting.thy Wed Jan 04 13:58:06 2012 +0100
@@ -75,7 +75,7 @@
fun invar :: "'a acom \<Rightarrow> 'a" where
"invar({I} WHILE b DO c {P}) = I"
-fun lift :: "('a set \<Rightarrow> 'a) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'a acom"
+fun lift :: "('a set \<Rightarrow> 'b) \<Rightarrow> com \<Rightarrow> 'a acom set \<Rightarrow> 'b acom"
where
"lift F com.SKIP M = (SKIP {F (post ` M)})" |
"lift F (x ::= a) M = (x ::= a {F (post ` M)})" |