--- a/src/HOL/TLA/Intensional.thy Mon Jul 06 20:36:38 2009 +0200
+++ b/src/HOL/TLA/Intensional.thy Mon Jul 06 21:24:30 2009 +0200
@@ -268,7 +268,7 @@
let
(* analogous to RS, but using matching instead of resolution *)
fun matchres tha i thb =
- case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
+ case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of
([th],_) => th
| ([],_) => raise THM("matchres: no match", i, [tha,thb])
| _ => raise THM("matchres: multiple unifiers", i, [tha,thb])