# HG changeset patch
# User wenzelm
# Date 936471925 -7200
# Node ID dc4f8d6ee0d2a24896bceb4531d147e941a2825f
# Parent  43cedde6d52adaf8d1fed0ebc1770ae55b3bac85
Library.equal_lists;

diff -r 43cedde6d52a -r dc4f8d6ee0d2 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sat Sep 04 21:05:01 1999 +0200
+++ b/src/Pure/Isar/calculation.ML	Sat Sep 04 21:05:25 1999 +0200
@@ -125,8 +125,7 @@
     val facts = Proof.the_facts state;
     val rules = Seq.of_list (if_none opt_rules [] @ get_local_rules state);
 
-    fun differ thms thms' =
-      length thms <> length thms' orelse exists2 (not o Thm.eq_thm) (thms, thms');
+    fun differ thms thms' = not (Library.equal_lists Thm.eq_thm (thms, thms'));
     fun combine thms =
       Seq.map Library.single (Seq.flat (Seq.map (Method.multi_resolve (thms @ facts)) rules));