# HG changeset patch
# User wenzelm
# Date 1662398592 -7200
# Node ID f1d75869022225143efb2a498562aea7f39db80d
# Parent  0982d0220b3157c9e0df10725e83d60247f70a4d
tuned signature;

diff -r 0982d0220b31 -r f1d758690222 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Sep 05 17:53:45 2022 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Sep 05 19:23:12 2022 +0200
@@ -506,10 +506,11 @@
       Conjunction.elim_balanced (length goal_propss) th
       |> map2 Conjunction.elim_balanced (map length goal_propss)
       handle THM _ => err_lost ();
+    val matcher =
+      Unify.matcher (Context.Proof ctxt)
+        (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (map Thm.prop_of (flat results));
     val _ =
-      Unify.matches_list (Context.Proof ctxt)
-        (map (Soft_Type_System.purge ctxt) (flat goal_propss)) (map Thm.prop_of (flat results))
-        orelse error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
+      is_none matcher andalso error ("Proved a different theorem:\n" ^ Thm.string_of_thm ctxt th);
 
     fun recover_result ([] :: pss) thss = [] :: recover_result pss thss
       | recover_result (_ :: pss) (ths :: thss) = ths :: recover_result pss thss
diff -r 0982d0220b31 -r f1d758690222 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Mon Sep 05 17:53:45 2022 +0200
+++ b/src/Pure/goal.ML	Mon Sep 05 19:23:12 2022 +0200
@@ -206,9 +206,9 @@
                 |> Thm.check_hyps (Context.Proof ctxt'))
               handle THM (msg, _, _) => err msg | ERROR msg => err msg;
           in
-            if Unify.matches_list (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res]
-            then res
-            else err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
+            if is_none (Unify.matcher (Context.Proof ctxt') [Thm.term_of stmt] [Thm.prop_of res])
+            then err ("Proved a different theorem: " ^ Syntax.string_of_term ctxt' (Thm.prop_of res))
+            else res
           end);
     val res =
       if immediate orelse schematic orelse not future orelse skip then result ()
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;
-