Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
check_conv now only performs beta-eta-normalization when equations
authorberghofe
Tue, 27 Nov 2007 15:47:40 +0100
changeset 25472 3276a14d06a6
parent 25471 ca009b7ce693
child 25473 812db0f215b3
check_conv now only performs beta-eta-normalization when equations cannot be combined just by transitivity.
src/Pure/meta_simplifier.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle