# HG changeset patch
# User berghofe
# Date 1035213803 -7200
# Node ID eec2582923f634de53333e58a96d41b9c240b7c4
# Parent  c71b905a852a2e4784f39777e834565d9cadc563
Eta contraction is now switched off when printing extracted program.

diff -r c71b905a852a -r eec2582923f6 src/HOL/Extraction/Warshall.thy
--- 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]}
 *}