diff -r cd3aafc1c631 -r a51ce445d498 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed May 13 18:41:39 2009 +0200
+++ b/src/Tools/quickcheck.ML	Wed May 13 18:41:40 2009 +0200
@@ -94,7 +94,7 @@
       error "Term to be tested contains type variables";
     val _ = null (Term.add_vars t []) orelse
       error "Term to be tested contains schematic variables";
-    val frees = map dest_Free (OldTerm.term_frees t);
+    val frees = Term.add_frees t [];
   in (map fst frees, list_abs_free (frees, t)) end
 
 fun test_term ctxt quiet generator_name size i t =