--- a/src/HOL/HOLCF/Universal.thy Sun Mar 11 13:39:16 2012 +0100
+++ b/src/HOL/HOLCF/Universal.thy Sun Mar 11 13:54:08 2012 +0100
@@ -291,8 +291,8 @@
text {* We use a locale to parameterize the construction over a chain
of approx functions on the type to be embedded. *}
-locale bifinite_approx_chain = approx_chain +
- constrains approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
+locale bifinite_approx_chain =
+ approx_chain approx for approx :: "nat \<Rightarrow> 'a::bifinite \<rightarrow> 'a"
begin
subsubsection {* Choosing a maximal element from a finite set *}