1.1 --- a/src/Pure/Pure.thy	Mon Jun 24 13:54:57 2013 +0200
     1.2 +++ b/src/Pure/Pure.thy	Mon Jun 24 17:03:53 2013 +0200
     1.3 @@ -93,6 +93,9 @@
     1.4    and "end" :: thy_end % "theory"
     1.5    and "realizers" "realizability" "extract_type" "extract" :: thy_decl
     1.6    and "find_theorems" "find_consts" :: diag
     1.7 +  and "ProofGeneral.process_pgip" "ProofGeneral.pr" "ProofGeneral.undo"
     1.8 +    "ProofGeneral.restart" "ProofGeneral.kill_proof" "ProofGeneral.inform_file_processed"
     1.9 +    "ProofGeneral.inform_file_retracted" :: control
    1.10  begin
    1.11  
    1.12  ML_file "Isar/isar_syn.ML"