# HG changeset patch
# User wenzelm
# Date 937926448 -7200
# Node ID 30327f9f6b4aed053f89b4ac22539e7dbca7f9c5
# Parent  af3a1fe87c428a9ba9587620eda2ff3e8a7a23a4
differ: compare actual props only (hyps may changed due to trivial steps involving assumptions);

diff -r af3a1fe87c42 -r 30327f9f6b4a src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Tue Sep 21 17:06:49 1999 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Sep 21 17:07:28 1999 +0200
@@ -125,7 +125,8 @@
     val facts = Proof.the_facts state;
     val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
 
-    fun differ thms thms' = not (Library.equal_lists Thm.eq_thm (thms, thms'));
+    val eq_prop = op aconv o pairself (#prop o Thm.rep_thm);
+    fun differ thms thms' = not (Library.equal_lists eq_prop (thms, thms'));
     fun combine thms =
       Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));