src/HOL/Tools/Mirabelle/mirabelle.ML

               if n mod mirabelle_stride = 0 then
                 let
                   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'}
                   else NONE
                 end