author | blanchet |
Mon, 26 Apr 2010 23:45:32 +0200 | |
changeset 36406 | 0a2d5138b77c |
parent 36405 | 05a8d79eb338 |
child 36407 | d733c1a624f4 |
--- 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