make cont_proc handle eta-contracted terms
authorhuffman
Tue, 06 Jan 2009 09:03:37 -0800
changeset 29373 6a19d9f6021d
parent 29372 df457e0d9a55
child 29374 ff4ba1ed4527
make cont_proc handle eta-contracted terms
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