# 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) =