diff -r 8915e3ce8655 -r 04414091f3b5 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Wed Aug 25 14:18:09 2010 +0200
+++ b/src/Pure/drule.ML	Wed Aug 25 15:12:49 2010 +0200
@@ -277,7 +277,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
+  if null (Thm.tpairs_of th) then th else
     case distinct Thm.eq_thm (Seq.list_of (Thm.flexflex_rule th)) of
       [th] => th
     | []   => raise THM("flexflex_unique: impossible constraints", 0, [th])