diff -r 6c942cf3bf68 -r 1155c06fa956 src/HOLCF/Cfun2.ML
--- a/src/HOLCF/Cfun2.ML	Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cfun2.ML	Fri May 31 19:55:19 1996 +0200
@@ -48,11 +48,11 @@
         (rtac Rep_Cfun 1)
         ]);
 
-val monofun_fapp2 = cont_fapp2 RS cont2mono;
+bind_thm ("monofun_fapp2", cont_fapp2 RS cont2mono);
 (* monofun(fapp(?fo1)) *)
 
 
-val contlub_fapp2 = cont_fapp2 RS cont2contlub;
+bind_thm ("contlub_fapp2", cont_fapp2 RS cont2contlub);
 (* contlub(fapp(?fo1)) *)
 
 (* ------------------------------------------------------------------------ *)
@@ -60,10 +60,10 @@
 (* looks nice with mixfix syntac                                            *)
 (* ------------------------------------------------------------------------ *)
 
-val cont_cfun_arg = (cont_fapp2 RS contE RS spec RS mp);
+bind_thm ("cont_cfun_arg", (cont_fapp2 RS contE RS spec RS mp));
 (* is_chain(?x1) ==> range (%i. ?fo3`(?x1 i)) <<| ?fo3`(lub (range ?x1))    *)
  
-val contlub_cfun_arg = (contlub_fapp2 RS contlubE RS spec RS mp);
+bind_thm ("contlub_cfun_arg", (contlub_fapp2 RS contlubE RS spec RS mp));
 (* is_chain(?x1) ==> ?fo4`(lub (range ?x1)) = lub (range (%i. ?fo4`(?x1 i))) *)
 
 
@@ -93,7 +93,7 @@
         ]);
 
 
-val monofun_cfun_arg = (monofun_fapp2 RS monofunE RS spec RS spec RS mp);
+bind_thm ("monofun_cfun_arg", monofun_fapp2 RS monofunE RS spec RS spec RS mp);
 (* ?x2 << ?x1 ==> ?fo5`?x2 << ?fo5`?x1                                      *)
 
 (* ------------------------------------------------------------------------ *)
@@ -125,7 +125,7 @@
         ]);
 
 
-val ch2ch_fappL = (monofun_fapp1 RS ch2ch_MF2L);
+bind_thm ("ch2ch_fappL", monofun_fapp1 RS ch2ch_MF2L);
 (* is_chain(?F) ==> is_chain (%i. ?F i`?x)                                  *)
 
 
@@ -210,7 +210,7 @@
         (etac (monofun_fapp1 RS ub2ub_monofun) 1)
         ]);
 
-val thelub_cfun = (lub_cfun RS thelubI);
+bind_thm ("thelub_cfun", lub_cfun RS thelubI);
 (* 
 is_chain(?CCF1) ==>  lub (range ?CCF1) = (LAM x. lub (range (%i. ?CCF1 i`x)))
 *)