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