--- 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
--- 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 ()
--- 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;
-