# HG changeset patch
# User desharna
# Date 1623918607 -7200
# Node ID eab5cd9c786206d62259f9ac62faf025e23efab0
# Parent  52b829b18066a2385bec05e978bb4e6b8e4706f0
changed Mirabelle's filter to use short theory names

diff -r 52b829b18066 -r eab5cd9c7862 src/HOL/Tools/Mirabelle/mirabelle.ML
--- 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;