# HG changeset patch
# User nipkow
# Date 1323718099 -3600
# Node ID fe518d5f35982680bf8fb9c56e3492ab76476fa9
# Parent  0b02adadf38417e35f3a3eff97f3ad23c235b6de
tuned

diff -r 0b02adadf384 -r fe518d5f3598 src/HOL/IMP/Sec_Typing.thy
--- a/src/HOL/IMP/Sec_Typing.thy	Sun Dec 11 18:22:06 2011 +0100
+++ b/src/HOL/IMP/Sec_Typing.thy	Mon Dec 12 20:28:19 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`