diff -r 8915e3ce8655 -r 04414091f3b5 src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Wed Aug 25 14:18:09 2010 +0200
+++ b/src/HOL/Tools/meson.ML	Wed Aug 25 15:12:49 2010 +0200
@@ -107,7 +107,7 @@
   | NONE => raise THM ("first_order_resolve", 0, [thA, thB]))
 
 fun flexflex_first_order th =
-  case (tpairs_of th) of
+  case Thm.tpairs_of th of
       [] => th
     | pairs =>
         let val thy = theory_of_thm th