src/Pure/ProofGeneral/proof_general_pgip.ML

 
 (* FIXME: Not quite same as commands used above *)
 val inform_file_processedP =
   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
     (P.name >> (fn file => Toplevel.no_timing o
-      Toplevel.keep (vacuous_inform_file_processed file) o
+      Toplevel.init_empty (vacuous_inform_file_processed file) o
       Toplevel.kill o
-      Toplevel.keep (proper_inform_file_processed file)));
+      Toplevel.init_empty (proper_inform_file_processed file)));
 
 val inform_file_retractedP =
   OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
     (P.name >> (Toplevel.no_timing oo
       (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));