changeset 31138 | a51ce445d498 |
parent 30980 | fe0855471964 |
child 31153 | 6b31b143f18b |
--- 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 =