--- a/src/HOLCF/Tools/cont_proc.ML Tue Jan 06 09:02:18 2009 -0800
+++ b/src/HOLCF/Tools/cont_proc.ML Tue Jan 06 09:03:37 2009 -0800
@@ -40,7 +40,8 @@
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;
@@ -85,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