--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML Thu Apr 16 13:48:10 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML Thu Apr 16 14:18:32 2015 +0200
@@ -377,7 +377,6 @@
Outer_Syntax.command @{command_keyword nitpick}
"try to find a counterexample for a given subgoal using Nitpick"
(parse_params -- Scan.optional Parse.nat 1 >> (fn (params, i) =>
- Toplevel.unknown_proof o
Toplevel.keep (fn state =>
ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
(Toplevel.proof_of state)))))