src/HOL/TLA/Intensional.ML
changeset 19861 620d90091788
parent 17309 c43ed29bd197
     1.1 --- a/src/HOL/TLA/Intensional.ML	Mon Jun 12 21:18:10 2006 +0200
     1.2 +++ b/src/HOL/TLA/Intensional.ML	Mon Jun 12 21:19:00 2006 +0200
     1.3 @@ -89,7 +89,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 (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])