src/Pure/PIDE/command.ML

       else if Keyword.is_proof name then Toplevel.reset_proof st0
       else NONE;
   in
     (case res of
       NONE => st0
-    | SOME st => (warning (Toplevel.type_error tr st0 ^ " -- resetting state"); st))
+    | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
   end) ();
 
 fun run int tr st =
   if Goal.future_enabled 1 andalso Keyword.is_diag (Toplevel.name_of tr) then
     (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}