src/HOLCF/LowerPD.thy
changeset 40327 1dfdbd66093a
parent 40321 d065b195ec89
child 40436 adb22dbb5242
--- a/src/HOLCF/LowerPD.thy	Fri Oct 29 16:51:40 2010 -0700
+++ b/src/HOLCF/LowerPD.thy	Fri Oct 29 17:15:28 2010 -0700
@@ -256,7 +256,7 @@
 lemma compact_lower_unit_iff [simp]: "compact {x}\<flat> \<longleftrightarrow> compact x"
 apply (safe elim!: compact_lower_unit)
 apply (simp only: compact_def lower_unit_below_iff [symmetric])
-apply (erule adm_subst [OF cont_Rep_CFun2])
+apply (erule adm_subst [OF cont_Rep_cfun2])
 done
 
 lemma compact_lower_plus [simp]: