# HG changeset patch
# User nipkow
# Date 1323718114 -3600
# Node ID 08e44ea5ac6932d550aa016a069f2c0799a3b6e7
# Parent  1fe2dd6d5086ea389670b8890fbefb21989e0fce# Parent  fe518d5f35982680bf8fb9c56e3492ab76476fa9
merged

diff -r 1fe2dd6d5086 -r 08e44ea5ac69 src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Mon Dec 12 19:47:50 2011 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy	Mon Dec 12 20:28:34 2011 +0100
@@ -100,7 +100,7 @@
     assume "\<not> sec_bexp b \<le> l"
     have 1: "sec_bexp b \<turnstile> IF b THEN c1 ELSE c2"
       by(rule sec_type.intros)(simp_all add: `sec_bexp b \<turnstile> c1` `sec_bexp b \<turnstile> c2`)
-    from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] `\<not> sec_bexp b \<le> l`
+    from confinement[OF IfTrue.hyps(2) `sec_bexp b \<turnstile> c1`] `\<not> sec_bexp b \<le> l`
     have "s = s' (\<le> l)" by auto
     moreover
     from confinement[OF IfTrue.prems(1) 1] `\<not> sec_bexp b \<le> l`