# HG changeset patch
# User wenzelm
# Date 1492597656 -7200
# Node ID a72ab197e68134b4257c988c054c5d718e87adcc
# Parent  decdb95bd007903b192b8452ff2b2f4f8ba33c45
proper base name, e.g. relevant for Code_Namespace.hierarchical_program;

diff -r decdb95bd007 -r a72ab197e681 src/Pure/theory.ML
--- a/src/Pure/theory.ML	Tue Apr 18 19:17:46 2017 +0200
+++ b/src/Pure/theory.ML	Wed Apr 19 12:27:36 2017 +0200
@@ -170,7 +170,7 @@
       thy
       |> init_markup (name, pos)
       |> Sign.local_path
-      |> Sign.map_naming (Name_Space.set_theory_name name)
+      |> Sign.map_naming (Name_Space.set_theory_name (Long_Name.base_name name))
       |> apply_wrappers wrappers
       |> tap (Syntax.force_syntax o Sign.syn_of)
     end;