# HG changeset patch # User huffman # Date 1231261338 28800 # Node ID df457e0d9a557625743b99b191a8c1e22745e08b # Parent bab4e907d881adb33286ed5378ac626f98d06670 implement is_closed_term using Term.loose_bvar diff -r bab4e907d881 -r df457e0d9a55 src/HOLCF/Tools/cont_proc.ML --- a/src/HOLCF/Tools/cont_proc.ML Mon Jan 05 15:26:57 2009 -0800 +++ b/src/HOLCF/Tools/cont_proc.ML Tue Jan 06 09:02:18 2009 -0800 @@ -33,14 +33,7 @@ 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) =