src/HOLCF/Library/Strict_Fun.thy

--- a/src/HOLCF/Library/Strict_Fun.thy	Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/Library/Strict_Fun.thy	Wed Nov 10 11:42:35 2010 -0800
@@ -173,7 +173,7 @@
 apply (erule (1) finite_deflation_sfun_map)
 done
 
-instantiation sfun :: (bifinite, bifinite) liftdomain
+instantiation sfun :: ("domain", "domain") liftdomain
 begin
 
 definition
@@ -210,7 +210,7 @@
 end
 
 lemma DEFL_sfun [domain_defl_simps]:
-  "DEFL('a::bifinite \<rightarrow>! 'b::bifinite) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
+  "DEFL('a \<rightarrow>! 'b) = sfun_defl\<cdot>DEFL('a)\<cdot>DEFL('b)"
 by (rule defl_sfun_def)
 
 lemma isodefl_sfun [domain_isodefl]: