src/Pure/raw_simplifier.ML
changeset 59690 46b635624feb
parent 59647 c6f413b660cf
child 60184 7541f29492c3
     1.1 --- a/src/Pure/raw_simplifier.ML	Fri Mar 13 12:58:49 2015 +0100
     1.2 +++ b/src/Pure/raw_simplifier.ML	Fri Mar 13 16:09:55 2015 +0100
     1.3 @@ -845,8 +845,15 @@
     1.4  fun check_conv ctxt msg thm thm' =
     1.5    let
     1.6      val thm'' = Thm.transitive thm thm' handle THM _ =>
     1.7 -     Thm.transitive thm (Thm.transitive
     1.8 -       (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm')
     1.9 +      let
    1.10 +        val nthm' =
    1.11 +          Thm.transitive (Thm.symmetric (Drule.beta_eta_conversion (Thm.lhs_of thm'))) thm'
    1.12 +      in Thm.transitive thm nthm' handle THM _ =>
    1.13 +           let
    1.14 +             val nthm =
    1.15 +               Thm.transitive thm (Drule.beta_eta_conversion (Thm.rhs_of thm))
    1.16 +           in Thm.transitive nthm nthm' end
    1.17 +      end
    1.18      val _ =
    1.19        if msg then cond_tracing ctxt (fn () => print_thm ctxt "SUCCEEDED" ("", thm'))
    1.20        else ();