# HG changeset patch
# User paulson
# Date 1117119020 -7200
# Node ID fbb5ae140535ddc0607fd5806e3294db8c5e9bd3
# Parent  9169bdf930f8a1e6ef14ac373c22d192db005dd3
goodby to modUnix

diff -r 9169bdf930f8 -r fbb5ae140535 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu May 26 16:50:07 2005 +0200
+++ b/src/HOL/IsaMakefile	Thu May 26 16:50:20 2005 +0200
@@ -92,7 +92,7 @@
   ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
   Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
   Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML		\
-  Tools/ATP/VampireCommunication.ML Tools/ATP/modUnix.ML			\
+  Tools/ATP/VampireCommunication.ML			\
   Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
   Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML			\
   Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
diff -r 9169bdf930f8 -r fbb5ae140535 src/HOL/Reconstruction.thy
--- a/src/HOL/Reconstruction.thy	Thu May 26 16:50:07 2005 +0200
+++ b/src/HOL/Reconstruction.thy	Thu May 26 16:50:20 2005 +0200
@@ -14,20 +14,19 @@
 	  "Tools/res_axioms.ML"
 	  "Tools/res_types_sorts.ML"
 
-          "Tools/ATP/recon_prelim.ML"
+      "Tools/ATP/recon_prelim.ML"
  	  "Tools/ATP/recon_order_clauses.ML"
  	  "Tools/ATP/recon_translate_proof.ML"
  	  "Tools/ATP/recon_parse.ML"
  	  "Tools/ATP/recon_transfer_proof.ML"
 	  "Tools/ATP/VampireCommunication.ML"
 	  "Tools/ATP/SpassCommunication.ML"
-	 (* "Tools/ATP/modUnix.ML"**)
 	  "Tools/ATP/watcher.sig"
 	  "Tools/ATP/watcher.ML"
 	  "Tools/ATP/res_clasimpset.ML"
 	  "Tools/res_atp.ML"
 
-          "Tools/reconstruction.ML"
+      "Tools/reconstruction.ML"
 
 begin