# HG changeset patch
# User haftmann
# Date 1312406513 -7200
# Node ID d5e28a49e16e42d6afe4e59373642d8b5aa240a5
# Parent  ec2a7901217b63c0786760a39bd333719fadae64
more specific instantiation

diff -r ec2a7901217b -r d5e28a49e16e src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Aug 03 23:21:52 2011 +0200
+++ b/src/HOL/Predicate.thy	Wed Aug 03 23:21:53 2011 +0200
@@ -431,7 +431,7 @@
   "x \<in> (op =) y \<longleftrightarrow> x = y"
   by (auto simp add: mem_def)
 
-instantiation pred :: (type) "{complete_lattice, boolean_algebra}"
+instantiation pred :: (type) complete_boolean_algebra
 begin
 
 definition