# HG changeset patch
# User haftmann
# Date 1256550702 -3600
# Node ID 616be6d7997ec55bbec68bd1c8f8437ba6d85caf
# Parent  607b702feace98539fce4e5e0dc46a6da6aa71b0
tuned

diff -r 607b702feace -r 616be6d7997e src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Mon Oct 26 10:51:42 2009 +0100
+++ b/src/Tools/Code/code_thingol.ML	Mon Oct 26 10:51:42 2009 +0100
@@ -399,7 +399,7 @@
 fun expand_eta thy k thm =
   let
     val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
-    val (head, args) = strip_comb lhs;
+    val (_, args) = strip_comb lhs;
     val l = if k = ~1
       then (length o fst o strip_abs) rhs
       else Int.max (0, k - length args);