author | blanchet |
Mon, 26 Apr 2010 21:14:28 +0200 | |
changeset 36397 | 2a5c6e7b55cb |
parent 36396 | 417cdfb2746a |
child 36398 | de8522a5cbae |
--- a/src/HOL/Tools/Nitpick/nitpick.ML Sun Apr 25 15:30:33 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Apr 26 21:14:28 2010 +0200 @@ -982,8 +982,6 @@ 0 => (priority "No subgoal!"; ("none", state)) | n => let - val (t, frees) = Logic.goal_params t i - val t = subst_bounds (frees, t) 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