src/HOLCF/Cprod2.ML

--- a/src/HOLCF/Cprod2.ML	Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cprod2.ML	Fri May 31 19:55:19 1996 +0200
@@ -160,7 +160,7 @@
         (etac (monofun_snd RS ub2ub_monofun) 1)
         ]);
 
-val thelub_cprod = (lub_cprod RS thelubI);
+bind_thm ("thelub_cprod", lub_cprod RS thelubI);
 (*
 "is_chain ?S1 ==>
  lub (range ?S1) =