src/HOLCF/Cont.ML

         (resolve_tac prems 1),
         (resolve_tac prems 1)
         ]);
 
 
-val cont2cont_app2 = (allI RSN (2,cont2cont_app));
+bind_thm ("cont2cont_app2", allI RSN (2,cont2cont_app));
 (*  [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *)
 (*        cont (%x. ?ft x (?tt x))                    *)
 
 
 (* ------------------------------------------------------------------------ *)