diff -r 17bf4ddd0833 -r 51c866d1b53b src/HOL/HOLCF/ConvexPD.thy
--- a/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 22 18:23:48 2010 -0800
+++ b/src/HOL/HOLCF/ConvexPD.thy	Wed Dec 22 18:24:04 2010 -0800
@@ -168,11 +168,11 @@
 
 definition
   convex_unit :: "'a \<rightarrow> 'a convex_pd" where
-  "convex_unit = compact_basis.basis_fun (\<lambda>a. convex_principal (PDUnit a))"
+  "convex_unit = compact_basis.extension (\<lambda>a. convex_principal (PDUnit a))"
 
 definition
   convex_plus :: "'a convex_pd \<rightarrow> 'a convex_pd \<rightarrow> 'a convex_pd" where
-  "convex_plus = convex_pd.basis_fun (\<lambda>t. convex_pd.basis_fun (\<lambda>u.
+  "convex_plus = convex_pd.extension (\<lambda>t. convex_pd.extension (\<lambda>u.
       convex_principal (PDPlus t u)))"
 
 abbreviation
@@ -190,13 +190,13 @@
 lemma convex_unit_Rep_compact_basis [simp]:
   "{Rep_compact_basis a}\<natural> = convex_principal (PDUnit a)"
 unfolding convex_unit_def
-by (simp add: compact_basis.basis_fun_principal PDUnit_convex_mono)
+by (simp add: compact_basis.extension_principal PDUnit_convex_mono)
 
 lemma convex_plus_principal [simp]:
   "convex_principal t +\<natural> convex_principal u = convex_principal (PDPlus t u)"
 unfolding convex_plus_def
-by (simp add: convex_pd.basis_fun_principal
-    convex_pd.basis_fun_mono PDPlus_convex_mono)
+by (simp add: convex_pd.extension_principal
+    convex_pd.extension_mono PDPlus_convex_mono)
 
 interpretation convex_add: semilattice convex_add proof
   fix xs ys zs :: "'a convex_pd"
@@ -342,7 +342,7 @@
 
 definition
   convex_bind :: "'a convex_pd \<rightarrow> ('a \<rightarrow> 'b convex_pd) \<rightarrow> 'b convex_pd" where
-  "convex_bind = convex_pd.basis_fun convex_bind_basis"
+  "convex_bind = convex_pd.extension convex_bind_basis"
 
 syntax
   "_convex_bind" :: "[logic, logic, logic] \<Rightarrow> logic"
@@ -354,7 +354,7 @@
 lemma convex_bind_principal [simp]:
   "convex_bind\<cdot>(convex_principal t) = convex_bind_basis t"
 unfolding convex_bind_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
 apply (erule convex_bind_basis_mono)
 done
 
@@ -521,12 +521,12 @@
 
 definition
   convex_to_upper :: "'a convex_pd \<rightarrow> 'a upper_pd" where
-  "convex_to_upper = convex_pd.basis_fun upper_principal"
+  "convex_to_upper = convex_pd.extension upper_principal"
 
 lemma convex_to_upper_principal [simp]:
   "convex_to_upper\<cdot>(convex_principal t) = upper_principal t"
 unfolding convex_to_upper_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
 apply (rule upper_pd.principal_mono)
 apply (erule convex_le_imp_upper_le)
 done
@@ -560,12 +560,12 @@
 
 definition
   convex_to_lower :: "'a convex_pd \<rightarrow> 'a lower_pd" where
-  "convex_to_lower = convex_pd.basis_fun lower_principal"
+  "convex_to_lower = convex_pd.extension lower_principal"
 
 lemma convex_to_lower_principal [simp]:
   "convex_to_lower\<cdot>(convex_principal t) = lower_principal t"
 unfolding convex_to_lower_def
-apply (rule convex_pd.basis_fun_principal)
+apply (rule convex_pd.extension_principal)
 apply (rule lower_pd.principal_mono)
 apply (erule convex_le_imp_lower_le)
 done