merged.
--- a/src/HOLCF/Tools/cont_proc.ML Tue Jan 06 13:36:42 2009 +0100
+++ b/src/HOLCF/Tools/cont_proc.ML Tue Jan 06 09:18:02 2009 -0800
@@ -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