# HG changeset patch
# User nipkow
# Date 1325681886 -3600
# Node ID b903d272c37dfd38a2a4bc66a1c8e6ade653562a
# Parent  ecab67f5a5c2e6ef08de4e7a991612dc0ecdc254
generalised type

diff -r ecab67f5a5c2 -r b903d272c37d src/HOL/IMP/Collecting.thy
--- 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)})" |