Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
A more robust flexflex_unique
authorpaulson
Wed, 20 Jun 2007 17:32:53 +0200
changeset 23439 8c7da8649f2f
parent 23438 dd824e86fa8a
child 23440 37860871f241
A more robust flexflex_unique
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle