diff -r 8fd9d555d04d -r fbdc860d87a3 src/HOL/ex/PER.thy
--- a/src/HOL/ex/PER.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/ex/PER.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -1,5 +1,4 @@
 (*  Title:      HOL/ex/PER.thy
-    ID:         $Id$
     Author:     Oscar Slotosch and Markus Wenzel, TU Muenchen
 *)
 
@@ -30,12 +29,10 @@
   but not necessarily reflexive.
 *}
 
-consts
-  eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
-
-axclass partial_equiv < type
-  partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
-  partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
+class partial_equiv =
+  fixes eqv :: "'a => 'a => bool"    (infixl "\<sim>" 50)
+  assumes partial_equiv_sym [elim?]: "x \<sim> y ==> y \<sim> x"
+  assumes partial_equiv_trans [trans]: "x \<sim> y ==> y \<sim> z ==> x \<sim> z"
 
 text {*
   \medskip The domain of a partial equivalence relation is the set of
@@ -70,7 +67,10 @@
   structural one corresponding to the congruence property.
 *}
 
-defs (overloaded)
+instantiation "fun" :: (partial_equiv, partial_equiv) partial_equiv
+begin
+
+definition
   eqv_fun_def: "f \<sim> g == \<forall>x \<in> domain. \<forall>y \<in> domain. x \<sim> y --> f x \<sim> g y"
 
 lemma partial_equiv_funI [intro?]:
@@ -86,8 +86,7 @@
   spaces (in \emph{both} argument positions).
 *}
 
-instance "fun" :: (partial_equiv, partial_equiv) partial_equiv
-proof
+instance proof
   fix f g h :: "'a::partial_equiv => 'b::partial_equiv"
   assume fg: "f \<sim> g"
   show "g \<sim> f"
@@ -110,6 +109,8 @@
   qed
 qed
 
+end
+
 
 subsection {* Total equivalence *}
 
@@ -120,8 +121,8 @@
   symmetric.
 *}
 
-axclass equiv < partial_equiv
-  eqv_refl [intro]: "x \<sim> x"
+class equiv =
+  assumes eqv_refl [intro]: "x \<sim> x"
 
 text {*
   On total equivalences all elements are reflexive, and congruence
@@ -150,7 +151,7 @@
   \emph{equivalence classes} over elements of the base type @{typ 'a}.
 *}
 
-typedef 'a quot = "{{x. a \<sim> x}| a::'a. True}"
+typedef 'a quot = "{{x. a \<sim> x}| a::'a::partial_equiv. True}"
   by blast
 
 lemma quotI [intro]: "{x. a \<sim> x} \<in> quot"