--- a/src/HOLCF/Sprod3.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Sprod3.ML Fri May 31 19:55:19 1996 +0200
@@ -612,7 +612,7 @@
]);
-val thelub_sprod2 = (lub_sprod2 RS thelubI);
+bind_thm ("thelub_sprod2", lub_sprod2 RS thelubI);
(*
"is_chain ?S1 ==>
lub (range ?S1) =