diff -r a8724924a62e -r 13ab4f0a0b0e Nominal/Nominal2_Base.thy
--- a/Nominal/Nominal2_Base.thy	Tue Mar 26 16:41:31 2013 +0100
+++ b/Nominal/Nominal2_Base.thy	Wed Mar 27 16:08:30 2013 +0100
@@ -769,7 +769,7 @@
 
 subsection {* Eqvt infrastructure *}
 
-text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
+text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw}. *}
 
 ML_file "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
@@ -1056,11 +1056,11 @@
   given.
 *}
 
-class le_eqvt = ord +
-  assumes le_eqvt [eqvt]: "p \<bullet> (x \<le> y) = ((p \<bullet> x) \<le> (p \<bullet> (y::('a::{order, pt}))))"
+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 = Inf +
-  assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::'a::{complete_lattice, pt} set))"
+  assumes inf_eqvt [eqvt]: "p \<bullet> (Inf X) = Inf (p \<bullet> (X::('a::{pt, complete_lattice}) set))"
 
 instantiation bool :: le_eqvt
 begin
@@ -3228,13 +3228,11 @@
   (@{const_name "atom"}, SOME @{typ "'a::at_base \<Rightarrow> atom"}) *}
 
 
-
 section {* Library functions for the nominal infrastructure *}
 
 ML_file "nominal_library.ML"
 
 
-
 section {* The freshness lemma according to Andy Pitts *}
 
 lemma freshness_lemma:
@@ -3417,18 +3415,16 @@
   shows "(FRESH x. P x \<or> Q x) \<longleftrightarrow> (FRESH x. P x) \<or> (FRESH x. Q x)"
 using P Q by (rule FRESH_binop_iff)
 
+
 section {* Automation for creating concrete atom types *}
 
-text {* at the moment only single-sort concrete atoms are supported *}
+text {* At the moment only single-sort concrete atoms are supported. *}
 
 ML_file "nominal_atoms.ML"
 
 
-section {* automatic equivariance procedure for inductive definitions *}
+section {* Automatic equivariance procedure for inductive definitions *}
 
 ML_file "nominal_eqvt.ML"
 
-
-
-
 end