Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/drule.ML
changeset 63068 8b9401bfd9fd
parent 62876 507c90523113
child 64556 851ae0e7b09c 
--- a/src/Pure/drule.ML	Thu Apr 28 11:47:01 2016 +0200
+++ b/src/Pure/drule.ML	Thu Apr 28 15:42:52 2016 +0200
@@ -447,8 +447,7 @@
 local
 
 fun contract_lhs th =
-  Thm.transitive (Thm.symmetric (beta_eta_conversion
-    (fst (Thm.dest_equals (Thm.cprop_of th))))) th;
+  Thm.transitive (Thm.symmetric (beta_eta_conversion (#1 (Thm.dest_equals (Thm.cprop_of th))))) th;
 
 fun var_args ct =
   (case try Thm.dest_comb ct of
isabelle