src/Pure/Pure.thy
changeset 58842 22b87ab47d3b
parent 58800 bfed1c26caed
child 58845 8451eddc4d67
--- a/src/Pure/Pure.thy	Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Pure/Pure.thy	Fri Oct 31 11:18:17 2014 +0100
@@ -100,9 +100,6 @@
   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"
@@ -117,7 +114,6 @@
 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"