1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 17:04:21 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 17:28:16 2010 +0200
     1.3 @@ -1817,20 +1817,18 @@
     1.4    end
     1.5  
     1.6  val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
     1.7 -
     1.8  fun wf_constraint_for rel side concl main =
     1.9    let
    1.10 -    val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
    1.11 -                                                tuple_for_args concl), Var rel)
    1.12 +    val core = HOLogic.mk_mem (HOLogic.mk_prod
    1.13 +                               (pairself tuple_for_args (main, concl)), Var rel)
    1.14      val t = List.foldl HOLogic.mk_imp core side
    1.15 -    val vars = filter (not_equal rel) (Term.add_vars t [])
    1.16 +    val vars = filter_out (curry (op =) rel) (Term.add_vars t [])
    1.17    in
    1.18      Library.foldl (fn (t', ((x, j), T)) =>
    1.19                        HOLogic.all_const T
    1.20                        $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
    1.21                    (t, vars)
    1.22    end
    1.23 -
    1.24  fun wf_constraint_for_triple rel (side, main, concl) =
    1.25    map (wf_constraint_for rel side concl) main |> foldr1 s_conj
    1.26