# HG changeset patch
# User wenzelm
# Date 1255897145 -7200
# Node ID e760950ba6c5536d86aeb6c690f0d3f67d59180e
# Parent  d2e48879e65af5bb81cccc708e336a5f4e4cff1f
fixed proof (cf. d1d4d7a08a66);

diff -r d2e48879e65a -r e760950ba6c5 src/HOLCF/Universal.thy
--- a/src/HOLCF/Universal.thy	Sun Oct 18 22:16:37 2009 +0200
+++ b/src/HOLCF/Universal.thy	Sun Oct 18 22:19:05 2009 +0200
@@ -805,7 +805,7 @@
 
 lemma basis_emb_prj_less: "ubasis_le (basis_emb (basis_prj x)) x"
 unfolding basis_prj_def
- apply (subst f_inv_f [where f=basis_emb])
+ apply (subst f_inv_onto_f [where f=basis_emb])
   apply (rule ubasis_until)
   apply (rule range_eqI [where x=compact_bot])
   apply simp