diff -r 6ef5ddf22d3a -r bab4e907d881 src/HOLCF/Tools/cont_proc.ML
--- a/src/HOLCF/Tools/cont_proc.ML	Mon Jan 05 07:54:16 2009 -0800
+++ b/src/HOLCF/Tools/cont_proc.ML	Mon Jan 05 15:26:57 2009 -0800
@@ -73,9 +73,9 @@
   fun lam [] = ([], cont_K)
     | lam (x::ys) =
     let
-      (* should use "standard" for thms that are used multiple times *)
+      (* should use "close_derivation" for thms that are used multiple times *)
       (* it seems to allow for sharing in explicit proof objects *)
-      val x' = standard (k x);
+      val x' = Thm.close_derivation (k x);
       val Lx = x' RS cont_L;
     in (map (fn y => SOME (k y RS Lx)) ys, x') end;