--- a/src/Tools/quickcheck.ML Wed Dec 31 00:08:13 2008 +0100
+++ b/src/Tools/quickcheck.ML Wed Dec 31 00:08:13 2008 +0100
@@ -70,11 +70,11 @@
fun prep_test_term t =
let
- val _ = (null (term_tvars t) andalso null (term_tfrees t)) orelse
+ val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
error "Term to be tested contains type variables";
- val _ = null (term_vars t) orelse
+ val _ = null (Term.add_vars t []) orelse
error "Term to be tested contains schematic variables";
- val frees = map dest_Free (term_frees t);
+ val frees = map dest_Free (OldTerm.term_frees t);
in (map fst frees, list_abs_free (frees, t)) end
fun test_term ctxt quiet generator_name size i t =