src/HOL/Library/refute.ML

 val _ =
   Outer_Syntax.improper_command @{command_spec "refute"}
     "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;
             val {goal = st, ...} = Proof.raw_goal (Toplevel.proof_of state);
           in refute_goal ctxt parms st i; () end)));