| changeset 77889 | 5db014c36f42 |
| parent 74561 | 8e6c973003c8 |
| child 77895 | 655bd3b0671b |
--- a/src/Pure/sign.ML Wed Apr 19 23:27:55 2023 +0200 +++ b/src/Pure/sign.ML Thu Apr 20 11:57:34 2023 +0200 @@ -514,7 +514,7 @@ val mandatory_path = map_naming o Name_Space.mandatory_path; val qualified_path = map_naming oo Name_Space.qualified_path; -fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy); +fun local_path thy = thy |> root_path |> add_path (Context.theory_base_name thy); fun init_naming thy = let