diff -r 290e1571c829 -r c8b20f615d6c src/HOLCF/Ssum.thy
--- a/src/HOLCF/Ssum.thy	Sun May 18 17:04:48 2008 +0200
+++ b/src/HOLCF/Ssum.thy	Mon May 19 23:49:20 2008 +0200
@@ -216,11 +216,12 @@
 
 subsection {* Strict sum is a bifinite domain *}
 
-instance "++" :: (bifinite, bifinite) approx ..
+instantiation "++" :: (bifinite, bifinite) bifinite
+begin
 
-defs (overloaded)
+definition
   approx_ssum_def:
-    "approx \<equiv> \<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y))"
+    "approx = (\<lambda>n. sscase\<cdot>(\<Lambda> x. sinl\<cdot>(approx n\<cdot>x))\<cdot>(\<Lambda> y. sinr\<cdot>(approx n\<cdot>y)))"
 
 lemma approx_sinl [simp]: "approx i\<cdot>(sinl\<cdot>x) = sinl\<cdot>(approx i\<cdot>x)"
 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
@@ -228,8 +229,7 @@
 lemma approx_sinr [simp]: "approx i\<cdot>(sinr\<cdot>x) = sinr\<cdot>(approx i\<cdot>x)"
 unfolding approx_ssum_def by (cases "x = \<bottom>") simp_all
 
-instance "++" :: (bifinite, bifinite) bifinite
-proof
+instance proof
   fix i :: nat and x :: "'a \<oplus> 'b"
   show "chain (\<lambda>i. approx i\<cdot>x)"
     unfolding approx_ssum_def by simp
@@ -248,3 +248,5 @@
 qed
 
 end
+
+end