# HG changeset patch
# User wenzelm
# Date 1211053584 -7200
# Node ID 7ca61b1ad8723b14c68892c032fab127e9e70588
# Parent  c398a386608219a5db2b3a50463b5d24558bb116
tuned proof;

diff -r c398a3866082 -r 7ca61b1ad872 src/HOL/Bali/DefiniteAssignmentCorrect.thy
--- a/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat May 17 21:46:22 2008 +0200
+++ b/src/HOL/Bali/DefiniteAssignmentCorrect.thy	Sat May 17 21:46:24 2008 +0200
@@ -4469,7 +4469,7 @@
     "\<And> l. \<lbrakk>abrupt s1 = Some (Jump (Break l)); normal s0\<rbrakk>
            \<Longrightarrow> brk A l \<subseteq> dom (locals (store s1))" and
     "\<lbrakk>abrupt s1 = Some (Jump Ret);normal s0\<rbrakk>\<Longrightarrow>Result \<in> dom (locals (store s1))"
-  using prems by - (drule (3) da_good_approx, simp)
+  using assms by - (drule (3) da_good_approx, simp)
 
 
 (* Same as above but with explicit environment;