--- a/src/HOL/Library/Preorder.thy Thu May 07 12:17:17 2009 +0200
+++ b/src/HOL/Library/Preorder.thy Thu May 07 16:22:34 2009 +0200
@@ -6,7 +6,7 @@
imports Orderings
begin
-context preorder
+class preorder_equiv = preorder
begin
definition equiv :: "'a \<Rightarrow> 'a \<Rightarrow> bool" where