Optimized and exported flexflex_unique.

--- a/src/Pure/drule.ML	Thu Sep 29 01:12:16 2005 +0200
+++ b/src/Pure/drule.ML	Thu Sep 29 12:30:30 2005 +0200
@@ -108,6 +108,7 @@
   val has_internal: tag list -> bool
   val impose_hyps: cterm list -> thm -> thm
   val satisfy_hyps: thm list -> thm -> thm
+  val flexflex_unique: thm -> thm
   val close_derivation: thm -> thm
   val local_standard: thm -> thm
   val compose_single: thm * int * thm -> thm
@@ -430,6 +431,7 @@
 (*Squash a theorem's flexflex constraints provided it can be done uniquely.
   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])