diff -r 0d3a62127057 -r 906de96ba68a src/HOL/Library/refute.ML
--- a/src/HOL/Library/refute.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/HOL/Library/refute.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -2969,7 +2969,7 @@
     "try to find a model that refutes a given subgoal"
     (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
-        Toplevel.keep (fn state =>
+        Toplevel.keep_proof (fn state =>
           let
             val ctxt = Toplevel.context_of state;
             val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);