src/HOL/Library/refute.ML

--- a/src/HOL/Library/refute.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/HOL/Library/refute.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -3202,6 +3202,7 @@
     "try to find a model that refutes a given subgoal"
     (scan_parms -- Scan.optional Parse.nat 1 >>
       (fn (parms, i) =>
+        Toplevel.unknown_proof o
         Toplevel.keep (fn state =>
           let
             val ctxt = Toplevel.context_of state;