# 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), []),