1.1 --- a/src/HOL/IMP/Abs_Int2.thy	Tue Feb 12 11:54:29 2013 +0100
     1.2 +++ b/src/HOL/IMP/Abs_Int2.thy	Tue Feb 12 12:22:44 2013 +0100
     1.3 @@ -105,8 +105,8 @@
     1.4    (if res then bfilter b1 True (bfilter b2 True S)
     1.5     else bfilter b1 False S \<squnion> bfilter b2 False S)" |
     1.6  "bfilter (Less e1 e2) res S =
     1.7 -  (let (res1,res2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
     1.8 -   in afilter e1 res1 (afilter e2 res2 S))"
     1.9 +  (let (a1,a2) = filter_less' res (aval'' e1 S) (aval'' e2 S)
    1.10 +   in afilter e1 a1 (afilter e2 a2 S))"
    1.11  
    1.12  lemma afilter_in_L: "S \<in> L X \<Longrightarrow> vars e \<subseteq> X \<Longrightarrow> afilter e a S \<in> L X"
    1.13  by(induction e arbitrary: a S)