# HG changeset patch
# User blanchet
# Date 1272318332 -7200
# Node ID 0a2d5138b77c5b337a9148f84058c8263e2c0352
# Parent  05a8d79eb338505e5b014442a2d0b3370beff3d1
fixes 2a5c6e7b55cb;
do not throw out the baby with the bath water

diff -r 05a8d79eb338 -r 0a2d5138b77c src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Apr 26 21:50:36 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Apr 26 23:45:32 2010 +0200
@@ -982,6 +982,7 @@
       0 => (priority "No subgoal!"; ("none", state))
     | n =>
       let
+        val t = Logic.goal_params t i |> fst
         val assms = map term_of (Assumption.all_assms_of ctxt)
         val (subst, assms, t) = extract_fixed_frees ctxt (assms, t)
       in pick_nits_in_term state params auto i n step subst assms t end