# HG changeset patch
# User berghofe
# Date 1127989830 -7200
# Node ID 7efbe0ec9d4c67a0e173eedfd845ddb0445b563a
# Parent  46c2091e51876f7aa13b169b56e440adde582ec4
Optimized and exported flexflex_unique.

diff -r 46c2091e5187 -r 7efbe0ec9d4c src/Pure/drule.ML
--- 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])