# HG changeset patch
# User paulson
# Date 1182353573 -7200
# Node ID 8c7da8649f2f5e8dd056a260f41cae5493fea8dc
# Parent  dd824e86fa8a6139576ecbf64d798759a54cf43d
A more robust flexflex_unique

diff -r dd824e86fa8a -r 8c7da8649f2f src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Jun 20 17:28:55 2007 +0200
+++ b/src/Pure/drule.ML	Wed Jun 20 17:32:53 2007 +0200
@@ -365,10 +365,10 @@
   This step can lose information.*)
 fun flexflex_unique th =
   if null (tpairs_of th) then th else
-    case Seq.chop 2 (flexflex_rule th) of
-      ([th],_) => th
-    | ([],_)   => raise THM("flexflex_unique: impossible constraints", 0, [th])
-    |      _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
+    case distinct Thm.eq_thm (Seq.list_of (flexflex_rule th)) of
+      [th] => th
+    | []   => raise THM("flexflex_unique: impossible constraints", 0, [th])
+    |  _   => raise THM("flexflex_unique: multiple unifiers", 0, [th]);
 
 fun close_derivation thm =
   if Thm.get_name thm = "" then Thm.put_name "" thm