# HG changeset patch
# User wenzelm
# Date 1623050821 -7200
# Node ID 6e9a47d3850c1e4bcf4a3a6e3c12fe535ec175ab
# Parent  c10fe904ac103eb2c638b50488b6072861321f94
more robust within session "HOL";

diff -r c10fe904ac10 -r 6e9a47d3850c src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sun Jun 06 21:39:26 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Mon Jun 07 09:27:01 2021 +0200
@@ -180,7 +180,8 @@
                   val name = Toplevel.name_of tr;
                   val pos = Toplevel.pos_of tr;
                 in
-                  if can (Proof.assert_backward o Toplevel.proof_of) st andalso
+                  if Context.proper_subthy (\<^theory>, thy) andalso
+                    can (Proof.assert_backward o Toplevel.proof_of) st andalso
                     member (op =) whitelist name andalso
                     check (Context.theory_long_name thy) pos
                   then SOME {name = name, pos = pos, pre = Toplevel.proof_of st, post = st'}