# HG changeset patch
# User berghofe
# Date 1196174860 -3600
# Node ID 3276a14d06a624aea4005b976d4cdfa286759bbf
# Parent  ca009b7ce693b7600a0c161d349005a46108d97e
check_conv now only performs beta-eta-normalization when equations
cannot be combined just by transitivity.

diff -r ca009b7ce693 -r 3276a14d06a6 src/Pure/meta_simplifier.ML
--- 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