src/HOL/Tools/Nitpick/nitpick_commands.ML
changeset 60190 906de96ba68a
parent 60094 96a4765ba7d1
child 60310 932221b62e89
--- a/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_commands.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -377,7 +377,7 @@
   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.keep (fn state =>
+      Toplevel.keep_proof (fn state =>
         ignore (pick_nits params Normal i (Toplevel.proof_position_of state)
           (Toplevel.proof_of state)))))