diff -r fdfbbb92dadf -r c9e39eafc7a0 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Fri Dec 07 15:07:56 2007 +0100
+++ b/src/HOL/Real/PReal.thy	Fri Dec 07 15:07:59 2007 +0100
@@ -211,12 +211,20 @@
 instance preal :: linorder
   by intro_classes (rule preal_le_linear)
 
-instance preal :: distrib_lattice
-  "inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal \<equiv> min"
-  "sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal  \<equiv> max"
+instantiation preal :: distrib_lattice
+begin
+
+definition
+  "(inf \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = min"
+
+definition
+  "(sup \<Colon> preal \<Rightarrow> preal \<Rightarrow> preal) = max"
+
+instance
   by intro_classes
     (auto simp add: inf_preal_def sup_preal_def min_max.sup_inf_distrib1)
 
+end
 
 subsection{*Properties of Addition*}