src/HOL/Tools/res_reconstruct.ML

--- a/src/HOL/Tools/res_reconstruct.ML	Mon Aug 31 19:28:37 2009 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML	Tue Sep 01 14:09:59 2009 +0200
@@ -557,7 +557,7 @@
     in (sendback_metis_nochained lemmas ^ "\n" ^ minimize_line name lemmas ^
       (if used_conj then ""
        else "\nWarning: Goal is provable because context is inconsistent."),
-       lemmas)
+       nochained lemmas)
     end;
 
   (* === Extracting structured Isar-proof === *)