src/HOLCF/Cprod3.ML

         (rtac cont_fst 1),
         (rtac lub_cprod 1),
         (atac 1)
         ]);
 
-val thelub_cprod2 = (lub_cprod2 RS thelubI);
+bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
 (*
 is_chain ?S1 ==>
  lub (range ?S1) =
  <lub (range (%i. cfst`(?S1 i))), lub (range (%i. csnd`(?S1 i)))>" 
 *)