--- a/src/HOLCF/Cont.ML Sat Nov 05 21:42:24 2005 +0100
+++ b/src/HOLCF/Cont.ML Sat Nov 05 21:50:37 2005 +0100
@@ -8,8 +8,7 @@
val cont2cont_app2 = thm "cont2cont_app2";
val cont2cont_app3 = thm "cont2cont_app3";
val cont2cont_app = thm "cont2cont_app";
-val cont2cont_CF1L_rev = thm "cont2cont_CF1L_rev";
-val cont2cont_CF1L = thm "cont2cont_CF1L";
+val cont2cont_fun = thm "cont2cont_fun";
val cont2cont_lambda = thm "cont2cont_lambda";
val cont2contlub_app = thm "cont2contlub_app";
val cont2contlubE = thm "cont2contlubE";
@@ -31,8 +30,8 @@
val flatdom_strict2cont = thm "flatdom_strict2cont";
val flatdom_strict2mono = thm "flatdom_strict2mono";
val mono2mono_app = thm "mono2mono_app";
-val mono2mono_MF1L_rev = thm "mono2mono_MF1L_rev";
-val mono2mono_MF1L = thm "mono2mono_MF1L";
+val mono2mono_fun = thm "mono2mono_fun";
+val mono2mono_lambda = thm "mono2mono_lambda";
val monocontlub2cont = thm "monocontlub2cont";
val monofun_def = thm "monofun_def";
val monofunE = thm "monofunE";