remove needless code that was copy-pasted from Quickcheck (where it made sense)
authorblanchet
Mon, 26 Apr 2010 21:14:28 +0200
changeset 36397 2a5c6e7b55cb
parent 36396 417cdfb2746a
child 36398 de8522a5cbae
remove needless code that was copy-pasted from Quickcheck (where it made sense)
src/HOL/Tools/Nitpick/nitpick.ML
--- 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