Fixed eta constraction issue in compose_witness

--- a/src/Pure/Isar/element.ML	Thu Dec 20 22:21:30 2007 +0100
+++ b/src/Pure/Isar/element.ML	Fri Dec 21 16:18:23 2007 +0100
@@ -303,7 +303,12 @@
   let
     val th' = Goal.conclude th;
     val A = Thm.cprem_of r 1;
-  in Thm.implies_elim r (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th') end;
+  in
+    Thm.implies_elim
+      (Conv.gconv_rule Drule.beta_eta_conversion 1 r)
+      (Conv.fconv_rule Drule.beta_eta_conversion
+        (Thm.instantiate (Thm.match (Thm.cprop_of th', A)) th'))
+  end;
 
 val mark_witness = Logic.protect;