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