diff -r c197b3c3e7fa -r ff570720ba1c src/HOL/IMP/Abs_Int1.thy
--- a/src/HOL/IMP/Abs_Int1.thy	Thu Aug 09 22:31:04 2012 +0200
+++ b/src/HOL/IMP/Abs_Int1.thy	Fri Aug 10 17:17:05 2012 +0200
@@ -143,7 +143,7 @@
   have 2: "step' (top c) C \<sqsubseteq> C" by(rule lpfpc_pfp[OF 1])
   have 3: "strip (\<gamma>\<^isub>c (step' (top c) C)) = c"
     by(simp add: strip_lpfp[OF _ 1])
-  have "lfp (step UNIV) c \<le> \<gamma>\<^isub>c (step' (top c) C)"
+  have "lfp c (step UNIV) \<le> \<gamma>\<^isub>c (step' (top c) C)"
   proof(rule lfp_lowerbound[simplified,OF 3])
     show "step UNIV (\<gamma>\<^isub>c (step' (top c) C)) \<le> \<gamma>\<^isub>c (step' (top c) C)"
     proof(rule step_preserves_le[OF _ _ `wt C (vars c)` wt_top])
@@ -151,7 +151,7 @@
       show "\<gamma>\<^isub>c (step' (top c) C) \<le> \<gamma>\<^isub>c C" by(rule mono_gamma_c[OF 2])
     qed
   qed
-  from this 2 show "lfp (step UNIV) c \<le> \<gamma>\<^isub>c C"
+  from this 2 show "lfp c (step UNIV) \<le> \<gamma>\<^isub>c C"
     by (blast intro: mono_gamma_c order_trans)
 qed