# HG changeset patch
# User wenzelm
# Date 962056769 -7200
# Node ID 45f8896faacdd74e5f935c382e46b32390aed7f1
# Parent  034cb4ac78b83ef9d6001e31be9688a8f9ed8378
eq_prop: eta contract;

diff -r 034cb4ac78b8 -r 45f8896faacd src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Mon Jun 26 16:54:38 2000 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Jun 26 23:59:29 2000 +0200
@@ -125,7 +125,7 @@
   let
     val facts = Proof.the_facts state;
 
-    val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
+    val eq_prop = op aconv o pairself (Pattern.eta_contract o #prop o Thm.rep_thm);
     fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
 
     fun combine thms =