# HG changeset patch
# User wenzelm
# Date 1231273063 -3600
# Node ID 68b45381123229fd117c5f4e2d821a696694f6fb
# Parent  ff4ba1ed4527c0b361c8add03433457a79d272da# Parent  98aaf2cd873fe884c4ee10230053cdf47051c458
merged

diff -r 98aaf2cd873f -r 68b453811232 src/HOLCF/Tools/cont_proc.ML
--- a/src/HOLCF/Tools/cont_proc.ML	Tue Jan 06 21:17:37 2009 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML	Tue Jan 06 21:17:43 2009 +0100
@@ -33,21 +33,15 @@
 val cont_R = @{thm cont_Rep_CFun2};
 
 (* checks whether a term contains no dangling bound variables *)
-val is_closed_term =
-  let
-    fun bound_less i (t $ u) =
-          bound_less i t andalso bound_less i u
-      | bound_less i (Abs (_, _, t)) = bound_less (i+1) t
-      | bound_less i (Bound n) = n < i
-      | bound_less i _ = true; (* Const, Free, and Var are OK *)
-  in bound_less 0 end;
+fun is_closed_term t = not (Term.loose_bvar (t, 0));
 
 (* checks whether a term is written entirely in the LCF sublanguage *)
 fun is_lcf_term (Const (@{const_name Rep_CFun}, _) $ t $ u) =
       is_lcf_term t andalso is_lcf_term u
   | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ Abs (_, _, t)) =
       is_lcf_term t
-  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ _) = false
+  | is_lcf_term (Const (@{const_name Abs_CFun}, _) $ t) =
+      is_lcf_term (Term.incr_boundvars 1 t $ Bound 0)
   | is_lcf_term (Bound _) = true
   | is_lcf_term t = is_closed_term t;
 
@@ -73,9 +67,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;
 
@@ -92,6 +86,12 @@
       val (cs, ls) = cont_thms1 b t;
       val (cs', l) = lam cs;
     in (cs', l::ls) end
+    | cont_thms1 b (Const (@{const_name Abs_CFun}, _) $ t) =
+    let
+      val t' = Term.incr_boundvars 1 t $ Bound 0;
+      val (cs, ls) = cont_thms1 b t';
+      val (cs', l) = lam cs;
+    in (cs', l::ls) end
     | cont_thms1 _ (Bound n) = (var n, [])
     | cont_thms1 _ _ = ([], []);
 in