src/HOL/Tools/meson.ML
changeset 38709 04414091f3b5
parent 38623 08a789ef8044
child 38786 e46e7a9cb622
--- 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