diff -r bdcffa8d8665 -r 0382f6877b98 src/HOL/Reconstruction.thy
--- a/src/HOL/Reconstruction.thy	Thu Sep 15 17:44:53 2005 +0200
+++ b/src/HOL/Reconstruction.thy	Thu Sep 15 17:45:17 2005 +0200
@@ -7,7 +7,7 @@
 header{*Attributes for Reconstructing External Resolution Proofs*}
 
 theory Reconstruction
-    imports Hilbert_Choice Map Infinite_Set Extraction
+    imports Hilbert_Choice Map Infinite_Set Commutative_Ring Extraction
     uses "Tools/res_lib.ML"
 
 	 "Tools/res_clause.ML"