--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Wed Jun 16 08:19:09 2021 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Thu Jun 17 10:30:07 2021 +0200
@@ -173,7 +173,8 @@
fun make_commands (thy_index, (thy, segments)) =
let
val thy_long_name = Context.theory_long_name thy;
- val check_thy = check_theory thy_long_name;
+ val thy_name = Context.theory_name thy;
+ val check_thy = check_theory thy_name;
fun make_command {command = tr, prev_state = st, state = st', ...} =
let
val name = Toplevel.name_of tr;