src/Pure/Pure.thy

   and "realizers" :: thy_decl == ""
   and "realizability" :: thy_decl == ""
   and "extract_type" "extract" :: thy_decl
   and "find_theorems" "find_consts" :: diag
   and "named_theorems" :: thy_decl
-  and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
-    "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
-    "ProofGeneral.inform_file_retracted" :: control
 begin
 
 ML_file "ML/ml_antiquotations.ML"
 ML_file "ML/ml_thms.ML"
 ML_file "Tools/print_operation.ML"

 ML_file "Tools/rule_insts.ML";
 ML_file "Tools/thm_deps.ML";
 ML_file "Tools/class_deps.ML"
 ML_file "Tools/find_theorems.ML"
 ML_file "Tools/find_consts.ML"
-ML_file "Tools/proof_general_pure.ML"
 ML_file "Tools/simplifier_trace.ML"
 ML_file "Tools/named_theorems.ML"
 
 
 section \<open>Basic attributes\<close>