Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
don't distinguish between "fixes" and other free variables -- this confuses users
authorblanchet
Mon, 21 Feb 2011 10:29:13 +0100
changeset 41789 7c7b68b06c1a
parent 41788 adfd365c7ea4
child 41790 56dcd46ddf7a
don't distinguish between "fixes" and other free variables -- this confuses users
src/HOL/Tools/Nitpick/nitpick.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:29:00 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:29:13 2011 +0100
@@ -289,8 +289,8 @@
        skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
        unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
        constr_cache = Unsynchronized.ref []}
-    val pseudo_frees = fold Term.add_frees assm_ts []
-    val real_frees = subtract (op =) pseudo_frees (Term.add_frees neg_t [])
+    val pseudo_frees = []
+    val real_frees = fold Term.add_frees (neg_t :: assm_ts) []
     val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
             raise NOT_SUPPORTED "schematic type variables"
     val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
isabelle