# HG changeset patch
# User blanchet
# Date 1275406096 -7200
# Node ID 49c45156c9e17ad9f475ac7ec635fe20dd0cbbde
# Parent  8ad1e3768b4f9cb1a27d35fd04dd8f464990ecb0
cosmetics

diff -r 8ad1e3768b4f -r 49c45156c9e1 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 17:04:21 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jun 01 17:28:16 2010 +0200
@@ -1817,20 +1817,18 @@
   end
 
 val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb
-
 fun wf_constraint_for rel side concl main =
   let
-    val core = HOLogic.mk_mem (HOLogic.mk_prod (tuple_for_args main,
-                                                tuple_for_args concl), Var rel)
+    val core = HOLogic.mk_mem (HOLogic.mk_prod
+                               (pairself tuple_for_args (main, concl)), Var rel)
     val t = List.foldl HOLogic.mk_imp core side
-    val vars = filter (not_equal rel) (Term.add_vars t [])
+    val vars = filter_out (curry (op =) rel) (Term.add_vars t [])
   in
     Library.foldl (fn (t', ((x, j), T)) =>
                       HOLogic.all_const T
                       $ Abs (x, T, abstract_over (Var ((x, j), T), t')))
                   (t, vars)
   end
-
 fun wf_constraint_for_triple rel (side, main, concl) =
   map (wf_constraint_for rel side concl) main |> foldr1 s_conj