# HG changeset patch
# User huffman
# Date 1231198017 28800
# Node ID bab4e907d881adb33286ed5378ac626f98d06670
# Parent  6ef5ddf22d3a59e0c1a5514546d9dca5ea61b3fd
use Thm.close_derivation instead of standard

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;