# HG changeset patch
# User wenzelm
# Date 1681987835 -7200
# Node ID 44d845b152148df3c3e00bfc40e97d57553f4e45
# Parent  f4cd6e3b5075d2e3fc69da453684e438b4f92a29
proper theory_long_name;

diff -r f4cd6e3b5075 -r 44d845b15214 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Apr 20 12:44:19 2023 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Thu Apr 20 12:50:35 2023 +0200
@@ -331,7 +331,7 @@
 
 fun thms_of all thy =
   filter
-    (fn th => (all orelse Thm.theory_base_name th = Context.theory_base_name thy)
+    (fn th => (all orelse Thm.theory_long_name th = Context.theory_long_name thy)
       (* andalso is_executable_thm thy th *))
     (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
 
diff -r f4cd6e3b5075 -r 44d845b15214 src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Apr 20 12:44:19 2023 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Thu Apr 20 12:50:35 2023 +0200
@@ -153,7 +153,7 @@
 fun theorems_of thy =
   filter (fn (name, th) =>
              not (is_forbidden_theorem name) andalso
-             Thm.theory_base_name th = Context.theory_base_name thy)
+             Thm.theory_long_name th = Context.theory_long_name thy)
          (Global_Theory.all_thms_of thy true)
 
 fun check_formulas tsp =