tuned
authorhaftmann
Mon Oct 26 10:51:42 2009 +0100 (2009-10-26)
changeset 33187616be6d7997e
parent 33186 607b702feace
child 33188 3802b3b7845f
tuned
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_thingol.ML	Mon Oct 26 10:51:42 2009 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Mon Oct 26 10:51:42 2009 +0100
     1.3 @@ -399,7 +399,7 @@
     1.4  fun expand_eta thy k thm =
     1.5    let
     1.6      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
     1.7 -    val (head, args) = strip_comb lhs;
     1.8 +    val (_, args) = strip_comb lhs;
     1.9      val l = if k = ~1
    1.10        then (length o fst o strip_abs) rhs
    1.11        else Int.max (0, k - length args);