--- 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;