# HG changeset patch
# User ballarin
# Date 1198250303 -3600
# Node ID 9da2343deb921e788a0aac6c1490bc3f5cfaca91
# Parent  b091cbae3e2acc41991eaeec1475cd034d70ddc0
Fixed eta constraction issue in compose_witness

diff -r b091cbae3e2a -r 9da2343deb92 src/Pure/Isar/element.ML
--- 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;