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