src/HOLCF/Cprod3.ML
changeset 1779 1155c06fa956
parent 1461 6bcb44e4d6e5
child 2033 639de962ded4
--- a/src/HOLCF/Cprod3.ML	Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Cprod3.ML	Fri May 31 19:55:19 1996 +0200
@@ -283,7 +283,7 @@
         (atac 1)
         ]);
 
-val thelub_cprod2 = (lub_cprod2 RS thelubI);
+bind_thm ("thelub_cprod2", lub_cprod2 RS thelubI);
 (*
 is_chain ?S1 ==>
  lub (range ?S1) =