src/HOL/Tools/Nitpick/nitpick.ML
changeset 41789 7c7b68b06c1a
parent 41772 27d4c768cf20
child 41791 01d722707a36
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:29:00 2011 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:29:13 2011 +0100
     1.3 @@ -289,8 +289,8 @@
     1.4         skolems = Unsynchronized.ref [], special_funs = Unsynchronized.ref [],
     1.5         unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
     1.6         constr_cache = Unsynchronized.ref []}
     1.7 -    val pseudo_frees = fold Term.add_frees assm_ts []
     1.8 -    val real_frees = subtract (op =) pseudo_frees (Term.add_frees neg_t [])
     1.9 +    val pseudo_frees = []
    1.10 +    val real_frees = fold Term.add_frees (neg_t :: assm_ts) []
    1.11      val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
    1.12              raise NOT_SUPPORTED "schematic type variables"
    1.13      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,