--- a/src/Pure/meta_simplifier.ML Tue Nov 27 15:44:49 2007 +0100
+++ b/src/Pure/meta_simplifier.ML Tue Nov 27 15:47:40 2007 +0100
@@ -828,8 +828,9 @@
fun check_conv msg ss thm thm' =
let
- val thm'' = transitive thm (transitive
- (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
+ val thm'' = transitive thm thm' handle THM _ =>
+ transitive thm (transitive
+ (symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
in if msg then trace_thm (fn () => "SUCCEEDED") ss thm' else (); SOME thm'' end
handle THM _ =>
let val {thy, prop = _ $ _ $ prop0, ...} = Thm.rep_thm thm in