--- a/Nominal/Nominal2_Base.thy	Mon Mar 11 16:37:54 2013 +0000
+++ b/Nominal/Nominal2_Base.thy	Tue Mar 26 16:41:31 2013 +0100
@@ -1056,11 +1056,11 @@
   given.
 *}
 
-class le_eqvt =  order + 
-  assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{pt, order}))))"
-
-class inf_eqvt = complete_lattice +
-  assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, Inf}) set))"
+class le_eqvt = ord +
+  assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{order, pt}))))"
+
+class inf_eqvt = Inf +
+  assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::'a::{complete_lattice, pt} set))"
 
 instantiation bool :: le_eqvt
 begin