# HG changeset patch
# User wenzelm
# Date 1266532713 -3600
# Node ID 214ec053128e2d845bc6746f259abcf92a3be9d6
# Parent  ef65a2218c3155633f0dfd0bad6000d7ebb0f59c
locale: more precise treatment of naming vs. binding;

diff -r ef65a2218c31 -r 214ec053128e src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Thu Feb 18 23:37:43 2010 +0100
+++ b/src/Pure/Isar/expression.ML	Thu Feb 18 23:38:33 2010 +0100
@@ -681,7 +681,7 @@
             |> def_pred abinding parms defs' exts exts';
           val (_, thy'') =
             thy'
-            |> Sign.mandatory_path (Binding.name_of abinding)
+            |> Sign.qualified_path true abinding
             |> PureThy.note_thmss ""
               [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
             ||> Sign.restore_naming thy';
@@ -695,7 +695,7 @@
             |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
           val (_, thy'''') =
             thy'''
-            |> Sign.mandatory_path (Binding.name_of binding)
+            |> Sign.qualified_path true binding
             |> PureThy.note_thmss ""
                  [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
                   ((Binding.conceal (Binding.name axiomsN), []),