# HG changeset patch
# User ballarin
# Date 1221560726 -7200
# Node ID fc420a5cf72e11541b230f0d2feb1cec838d27b0
# Parent  f14f34194f63d8717e2f4a5ebb506bbfca8502a1
Do not rely on locale assumption in interpretation.

diff -r f14f34194f63 -r fc420a5cf72e src/HOLCF/Bifinite.thy
--- 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)