src/HOL/TLA/Intensional.thy
changeset 31945 d5f186aa0bed
parent 31460 d97fa41cc600
child 35108 e384e27c229f
     1.1 --- a/src/HOL/TLA/Intensional.thy	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.thy	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -268,7 +268,7 @@
     1.4    let
     1.5      (* analogous to RS, but using matching instead of resolution *)
     1.6      fun matchres tha i thb =
     1.7 -      case Seq.chop 2 (biresolution true [(false,tha)] i thb) of
     1.8 +      case Seq.chop 2 (Thm.biresolution true [(false,tha)] i thb) of
     1.9            ([th],_) => th
    1.10          | ([],_)   => raise THM("matchres: no match", i, [tha,thb])
    1.11          |      _   => raise THM("matchres: multiple unifiers", i, [tha,thb])