1.1 --- a/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 05 17:47:52 2007 +0100
     1.2 +++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 05 17:48:04 2007 +0100
     1.3 @@ -31,11 +31,11 @@
     1.4  
     1.5  lemmas disj_ac =
     1.6    disj_assoc disj_commute
     1.7 -  mk_left_commute [of "disj", OF disj_assoc disj_commute]
     1.8 +  mk_left_commute [where 'a = 'a, of "disj", OF disj_assoc disj_commute]
     1.9  
    1.10  lemmas conj_ac =
    1.11    conj_assoc conj_commute
    1.12 -  mk_left_commute [of "conj", OF conj_assoc conj_commute]
    1.13 +  mk_left_commute [where 'a = 'a, of "conj", OF conj_assoc conj_commute]
    1.14  
    1.15  lemma dual: "boolean disj conj compl one zero"
    1.16  apply (rule boolean.intro)
    1.17 @@ -206,7 +206,7 @@
    1.18  
    1.19  lemmas xor_ac =
    1.20    xor_assoc xor_commute
    1.21 -  mk_left_commute [of "xor", OF xor_assoc xor_commute]
    1.22 +  mk_left_commute [where 'a = 'a, of "xor", OF xor_assoc xor_commute]
    1.23  
    1.24  lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
    1.25  by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)