# HG changeset patch
# User wenzelm
# Date 1627392714 -7200
# Node ID dc98bb7a439bf45b9849030d62e7ab1f8aa1582f
# Parent  ffbd1b7e54397f551fc71143347758aaef9a552a# Parent  b25b7c264a93875bd3039459e863e9f5c9b8a0ec
merged

diff -r b25b7c264a93 -r dc98bb7a439b src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Jul 27 15:20:20 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Jul 27 15:31:54 2021 +0200
@@ -134,7 +134,10 @@
 
 fun check_theories strs =
   let
-    val theories = map read_theory_range strs;
+    fun theory_import_name s =
+      #theory_name (Resources.import_name (Session.get_name ()) Path.current s);
+    val theories = map read_theory_range strs
+      |> map (apfst theory_import_name);
     fun get_theory name =
       if null theories then SOME NONE
       else get_first (fn (a, b) => if a = name then SOME b else NONE) theories;
@@ -173,8 +176,7 @@
           fun make_commands (thy_index, (thy, segments)) =
             let
               val thy_long_name = Context.theory_long_name thy;
-              val thy_name = Context.theory_name thy;
-              val check_thy = check_theory thy_name;
+              val check_thy = check_theory thy_long_name;
               fun make_command {command = tr, prev_state = st, state = st', ...} =
                 let
                   val name = Toplevel.name_of tr;