Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/quickcheck.ML
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 =
isabelle