# 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; -