--- a/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 10 09:59:08 2010 -0800
+++ b/src/HOLCF/ex/Domain_Proofs.thy Wed Nov 10 11:42:35 2010 -0800
@@ -94,7 +94,7 @@
text {* Prove rep instance using lemma @{text typedef_rep_class}. *}
-instantiation foo :: (bifinite) liftdomain
+instantiation foo :: ("domain") liftdomain
begin
definition emb_foo :: "'a foo \<rightarrow> udom"
@@ -129,7 +129,7 @@
end
-instantiation bar :: (bifinite) liftdomain
+instantiation bar :: ("domain") liftdomain
begin
definition emb_bar :: "'a bar \<rightarrow> udom"
@@ -164,7 +164,7 @@
end
-instantiation baz :: (bifinite) liftdomain
+instantiation baz :: ("domain") liftdomain
begin
definition emb_baz :: "'a baz \<rightarrow> udom"