--- 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)))
--- 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 =