diff -r 666c3751227c -r c5b5f7a3a3b1 src/HOLCF/Library/Strict_Fun.thy
--- a/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 16:24:44 2010 -0700
+++ b/src/HOLCF/Library/Strict_Fun.thy	Mon Oct 11 21:35:31 2010 -0700
@@ -37,13 +37,13 @@
   unfolding sfun_rep_beta by (rule Rep_sfun [simplified])
 
 lemma strictify_cancel: "f\<cdot>\<bottom> = \<bottom> \<Longrightarrow> strictify\<cdot>f = f"
-  by (simp add: expand_cfun_eq strictify_conv_if)
+  by (simp add: cfun_eq_iff strictify_conv_if)
 
 lemma sfun_abs_sfun_rep: "sfun_abs\<cdot>(sfun_rep\<cdot>f) = f"
   unfolding sfun_abs_def sfun_rep_def
   apply (simp add: cont_Abs_sfun cont_Rep_sfun)
   apply (simp add: Rep_sfun_inject [symmetric] Abs_sfun_inverse)
-  apply (simp add: expand_cfun_eq strictify_conv_if)
+  apply (simp add: cfun_eq_iff strictify_conv_if)
   apply (simp add: Rep_sfun [simplified])
   done
 
@@ -56,7 +56,7 @@
 lemma ep_pair_sfun: "ep_pair sfun_rep sfun_abs"
 apply default
 apply (rule sfun_abs_sfun_rep)
-apply (simp add: expand_cfun_below strictify_conv_if)
+apply (simp add: cfun_below_iff strictify_conv_if)
 done
 
 interpretation sfun: ep_pair sfun_rep sfun_abs
@@ -71,14 +71,14 @@
 
 lemma sfun_map_ID: "sfun_map\<cdot>ID\<cdot>ID = ID"
   unfolding sfun_map_def
-  by (simp add: cfun_map_ID expand_cfun_eq)
+  by (simp add: cfun_map_ID cfun_eq_iff)
 
 lemma sfun_map_map:
   assumes "f2\<cdot>\<bottom> = \<bottom>" and "g2\<cdot>\<bottom> = \<bottom>" shows
   "sfun_map\<cdot>f1\<cdot>g1\<cdot>(sfun_map\<cdot>f2\<cdot>g2\<cdot>p) =
     sfun_map\<cdot>(\<Lambda> x. f2\<cdot>(f1\<cdot>x))\<cdot>(\<Lambda> x. g1\<cdot>(g2\<cdot>x))\<cdot>p"
 unfolding sfun_map_def
-by (simp add: expand_cfun_eq strictify_cancel assms cfun_map_map)
+by (simp add: cfun_eq_iff strictify_cancel assms cfun_map_map)
 
 lemma ep_pair_sfun_map:
   assumes 1: "ep_pair e1 p1"
@@ -193,7 +193,7 @@
 next
   show "cast\<cdot>DEFL('a \<rightarrow>! 'b) = emb oo (prj :: udom \<rightarrow> 'a \<rightarrow>! 'b)"
     unfolding emb_sfun_def prj_sfun_def defl_sfun_def cast_sfun_defl
-    by (simp add: cast_DEFL oo_def expand_cfun_eq sfun_map_map)
+    by (simp add: cast_DEFL oo_def cfun_eq_iff sfun_map_map)
 qed
 
 end