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