# HG changeset patch
# User nipkow
# Date 1366799188 -7200
# Node ID e117d4538233470ca69573058dd89bbabc4b6cf3
# Parent  199ce8cf604c19dd7d26e120f39164967558fc35# Parent  39133c710fa351d242a63878a3c43996412fb86b
merged

diff -r 199ce8cf604c -r e117d4538233 src/HOL/IMP/Abs_Int0.thy
--- a/src/HOL/IMP/Abs_Int0.thy	Wed Apr 24 12:15:06 2013 +0200
+++ b/src/HOL/IMP/Abs_Int0.thy	Wed Apr 24 12:26:28 2013 +0200
@@ -465,16 +465,16 @@
   for \<gamma> :: "'av::semilattice \<Rightarrow> val set" and m :: "'av \<Rightarrow> nat"
 begin
 
-lemma top_on_step': "\<lbrakk> vars C \<subseteq> X; top_on_acom (-X) C \<rbrakk> \<Longrightarrow> top_on_acom (-X) (step' \<top> C)"
+lemma top_on_step': "top_on_acom (-vars C) C \<Longrightarrow> top_on_acom (-vars C) (step' \<top> C)"
 unfolding step'_def
 by(rule top_on_Step)
   (auto simp add: top_option_def fa_def split: option.splits)
 
 lemma AI_Some_measure: "\<exists>C. AI c = Some C"
 unfolding AI_def
-apply(rule pfp_termination[where I = "\<lambda>C. strip C = c \<and> top_on_acom (- vars C) C" and m="m_c"])
+apply(rule pfp_termination[where I = "\<lambda>C. top_on_acom (- vars C) C" and m="m_c"])
 apply(simp_all add: m_c2 mono_step'_top bot_least top_on_bot)
-apply(auto simp add: top_on_step' vars_acom_def)
+using top_on_step' apply(auto simp add: vars_acom_def)
 done
 
 end