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