Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
--- a/src/HOL/IsaMakefile Sat Jun 03 17:49:42 2006 +0200
+++ b/src/HOL/IsaMakefile Sun Jun 04 10:50:41 2006 +0200
@@ -99,7 +99,7 @@
Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML \
Tools/ATP/recon_transfer_proof.ML \
Tools/ATP/reduce_axiomsN.ML \
- Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML \
+ Tools/ATP/recon_translate_proof.ML \
Tools/ATP/watcher.ML \
Tools/cnf_funcs.ML \
Tools/datatype_abs_proofs.ML Tools/datatype_aux.ML \
--- a/src/HOL/Reconstruction.thy Sat Jun 03 17:49:42 2006 +0200
+++ b/src/HOL/Reconstruction.thy Sun Jun 04 10:50:41 2006 +0200
@@ -19,7 +19,6 @@
"Tools/ATP/AtpCommunication.ML"
"Tools/ATP/watcher.ML"
"Tools/ATP/reduce_axiomsN.ML"
- "Tools/ATP/res_clasimpset.ML"
"Tools/res_atp.ML"
"Tools/reconstruction.ML"