# HG changeset patch
# User huffman
# Date 1287073685 25200
# Node ID f13341a4540738a2b75e7d74ca159a51aafdb286
# Parent  b974cf829099a2dc33fe6efa7b38d713c75fd26b
add type annotation to avoid warning

diff -r b974cf829099 -r f13341a45407 src/HOLCF/Bifinite.thy
--- a/src/HOLCF/Bifinite.thy	Wed Oct 13 10:56:42 2010 -0700
+++ b/src/HOLCF/Bifinite.thy	Thu Oct 14 09:28:05 2010 -0700
@@ -440,7 +440,7 @@
 
 lemma finite_deflation_lift_approx: "finite_deflation (lift_approx i)"
 proof
-  fix x
+  fix x :: "'a lift"
   show "lift_approx i\<cdot>x \<sqsubseteq> x"
     unfolding lift_approx_def
     by (cases x, simp, simp)