src/HOLCF/Sprod2.ML

         (cut_facts_tac prems 1),
         (rtac less_sprod2b 1),
         (etac (inst_sprod_po RS subst) 1)
         ]);
 
-val less_sprod4a = (less_sprod4b RS defined_Ispair_rev);
+bind_thm ("less_sprod4a", less_sprod4b RS defined_Ispair_rev);
 (* Ispair ?a ?b << Ispair UU UU ==> ?a = UU | ?b = UU *)
 
 qed_goal "less_sprod4c" Sprod2.thy
  "[|Ispair xa ya << Ispair x y; xa~=UU; ya~=UU; x~=UU; y~=UU|] ==>\
 \               xa<<x & ya << y"

         (rtac is_lub_thelub 1),
         (etac (monofun_Issnd RS ch2ch_monofun) 1),
         (etac (monofun_Issnd RS ub2ub_monofun) 1)
         ]);
 
-val thelub_sprod = (lub_sprod RS thelubI);
+bind_thm ("thelub_sprod", lub_sprod RS thelubI);
 
 
 qed_goal "cpo_sprod" Sprod2.thy 
         "is_chain(S::nat=>'a**'b)==>? x.range(S)<<| x"
 (fn prems =>