# HG changeset patch
# User huffman
# Date 1231261417 28800
# Node ID 6a19d9f6021ddd1268d30daa654c586ef69541d3
# Parent  df457e0d9a557625743b99b191a8c1e22745e08b
make cont_proc handle eta-contracted terms

diff -r df457e0d9a55 -r 6a19d9f6021d src/HOLCF/Tools/cont_proc.ML
--- 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