# HG changeset patch
# User paulson
# Date 1129282574 -7200
# Node ID 6fd3261a1be0da97fb1db7fddd3b123f459725d1
# Parent  1438291d57f0d912dbda2a4f7f899e31c05d23d2
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses

diff -r 1438291d57f0 -r 6fd3261a1be0 src/HOL/IsaMakefile
--- 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		\
diff -r 1438291d57f0 -r 6fd3261a1be0 src/HOL/Reconstruction.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"