Eta contraction is now switched off when printing extracted program.

--- a/src/HOL/Extraction/Warshall.thy	Mon Oct 21 17:20:29 2002 +0200
+++ b/src/HOL/Extraction/Warshall.thy	Mon Oct 21 17:23:23 2002 +0200
@@ -250,7 +250,7 @@
 
 text {*
   The program extracted from the above proof looks as follows
-  @{thm [display] warshall_def [no_vars]}
+  @{thm [display, eta_contract=false] warshall_def [no_vars]}
   The corresponding correctness theorem is
   @{thm [display] warshall_correctness [no_vars]}
 *}