# HG changeset patch
# User ballarin
# Date 1194281284 -3600
# Node ID c532fd8445a2c19f734c98c530c1896f7355d59d
# Parent  1cc04c8e1253c89f6a0b36d733b05c390a6de014
Type instance of thm mk_left_commute in locales.

diff -r 1cc04c8e1253 -r c532fd8445a2 src/HOL/Library/Boolean_Algebra.thy
--- a/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 05 17:47:52 2007 +0100
+++ b/src/HOL/Library/Boolean_Algebra.thy	Mon Nov 05 17:48:04 2007 +0100
@@ -31,11 +31,11 @@
 
 lemmas disj_ac =
   disj_assoc disj_commute
-  mk_left_commute [of "disj", OF disj_assoc disj_commute]
+  mk_left_commute [where 'a = 'a, of "disj", OF disj_assoc disj_commute]
 
 lemmas conj_ac =
   conj_assoc conj_commute
-  mk_left_commute [of "conj", OF conj_assoc conj_commute]
+  mk_left_commute [where 'a = 'a, of "conj", OF conj_assoc conj_commute]
 
 lemma dual: "boolean disj conj compl one zero"
 apply (rule boolean.intro)
@@ -206,7 +206,7 @@
 
 lemmas xor_ac =
   xor_assoc xor_commute
-  mk_left_commute [of "xor", OF xor_assoc xor_commute]
+  mk_left_commute [where 'a = 'a, of "xor", OF xor_assoc xor_commute]
 
 lemma xor_zero_right [simp]: "x \<oplus> \<zero> = x"
 by (simp only: xor_def compl_zero conj_one_right conj_zero_right disj_zero_right)