diff -r 0982d0220b31 -r f1d758690222 src/Pure/more_unify.ML
--- a/src/Pure/more_unify.ML	Mon Sep 05 17:53:45 2022 +0200
+++ b/src/Pure/more_unify.ML	Mon Sep 05 19:23:12 2022 +0200
@@ -8,7 +8,7 @@
 sig
   include UNIFY
   val matchers: Context.generic -> (term * term) list -> Envir.env Seq.seq
-  val matches_list: Context.generic -> term list -> term list -> bool
+  val matcher: Context.generic -> term list -> term list -> Envir.env option
 end;
 
 structure Unify: UNIFY =
@@ -75,11 +75,10 @@
           (first_order_matchers thy pairs empty)
       end;
 
-fun matches_list context ps os =
-  length ps = length os andalso is_some (Seq.pull (matchers context (ps ~~ os)));
-
+fun matcher context ps os =
+  if length ps <> length os then NONE
+  else Seq.pull (matchers context (ps ~~ os)) |> Option.map #1;
 
 open Unify;
 
 end;
-