Do not rely on locale assumption in interpretation.

--- a/src/HOLCF/Bifinite.thy	Tue Sep 16 12:25:04 2008 +0200
+++ b/src/HOLCF/Bifinite.thy	Tue Sep 16 12:25:26 2008 +0200
@@ -41,8 +41,10 @@
 interpretation approx: finite_deflation ["approx i"]
 by (rule finite_deflation_approx)
 
+lemma (in deflation) deflation: "deflation d" ..
+
 lemma deflation_approx: "deflation (approx i)"
-by (rule approx.deflation_axioms)
+by (rule approx.deflation)
 
 lemma lub_approx [simp]: "(\<Squnion>i. approx i) = (\<Lambda> x. x)"
 by (rule ext_cfun, simp add: contlub_cfun_fun)