src/HOL/Algebra/abstract/Ideal2.thy

--- a/src/HOL/Algebra/abstract/Ideal2.thy	Mon Feb 22 17:02:39 2010 +0100
+++ b/src/HOL/Algebra/abstract/Ideal2.thy	Tue Feb 23 10:11:12 2010 +0100
@@ -1,6 +1,5 @@
 (*
     Ideals for commutative rings
-    $Id$
     Author: Clemens Ballarin, started 24 September 1999
 *)
 
@@ -23,9 +22,8 @@
 
 text {* Principle ideal domains *}
 
-axclass pid < "domain"
-  pid_ax: "is_ideal I ==> is_pideal I"
-
+class pid =
+  assumes pid_ax: "is_ideal (I :: 'a::domain \<Rightarrow> _) \<Longrightarrow> is_pideal I"
 
 (* is_ideal *)