# HG changeset patch
# User blanchet
# Date 1298280553 -3600
# Node ID 7c7b68b06c1a037d704b58b42318962f936b4e39
# Parent  adfd365c7ea4b63514cb618913b72f289bcfcb8c
don't distinguish between "fixes" and other free variables -- this confuses users

diff -r adfd365c7ea4 -r 7c7b68b06c1a src/HOL/Tools/Nitpick/nitpick.ML
--- 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,