--- a/src/HOL/IsaMakefile Fri Oct 14 10:19:50 2005 +0200
+++ b/src/HOL/IsaMakefile Fri Oct 14 11:36:14 2005 +0200
@@ -107,7 +107,7 @@
Tools/recdef_package.ML Tools/recfun_codegen.ML \
Tools/reconstruction.ML Tools/record_package.ML Tools/refute.ML \
Tools/refute_isar.ML Tools/res_atp.ML Tools/res_axioms.ML \
- Tools/res_clause.ML Tools/res_types_sorts.ML Tools/rewrite_hol_proof.ML \
+ Tools/res_clause.ML Tools/rewrite_hol_proof.ML \
Tools/sat_funcs.ML \
Tools/sat_solver.ML Tools/specification_package.ML Tools/split_rule.ML \
Tools/typedef_package.ML Transitive_Closure.ML Transitive_Closure.thy \
--- a/src/HOL/Reconstruction.thy Fri Oct 14 10:19:50 2005 +0200
+++ b/src/HOL/Reconstruction.thy Fri Oct 14 11:36:14 2005 +0200
@@ -10,7 +10,6 @@
imports Hilbert_Choice Map Infinite_Set Extraction
uses "Tools/res_clause.ML"
"Tools/res_axioms.ML"
- "Tools/res_types_sorts.ML"
"Tools/ATP/recon_order_clauses.ML"
"Tools/ATP/recon_translate_proof.ML"
"Tools/ATP/recon_parse.ML"