--- a/src/HOLCF/Cfun3.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cfun3.ML Fri May 31 19:55:19 1996 +0200
@@ -183,7 +183,7 @@
(* lemma for the cont tactic *)
(* ------------------------------------------------------------------------ *)
-val cont2cont_LAM2 = (allI RSN (2,(allI RS cont2cont_LAM)));
+bind_thm ("cont2cont_LAM2", allI RSN (2,(allI RS cont2cont_LAM)));
(*
[| !!x. cont (?c1.0 x);
!!y. cont (%x. ?c1.0 x y) |] ==> cont (%x. LAM y. ?c1.0 x y)
@@ -343,10 +343,10 @@
]);
-val cont_Istrictify1 = (contlub_Istrictify1 RS
+bind_thm ("cont_Istrictify1", contlub_Istrictify1 RS
(monofun_Istrictify1 RS monocontlub2cont));
-val cont_Istrictify2 = (contlub_Istrictify2 RS
+bind_thm ("cont_Istrictify2", contlub_Istrictify2 RS
(monofun_Istrictify2 RS monocontlub2cont));