locale: more precise treatment of naming vs. binding;
authorwenzelm
Thu Feb 18 23:38:33 2010 +0100 (2010-02-18)
changeset 35204214ec053128e
parent 35203 ef65a2218c31
child 35205 611b90bb89bc
locale: more precise treatment of naming vs. binding;
src/Pure/Isar/expression.ML
     1.1 --- a/src/Pure/Isar/expression.ML	Thu Feb 18 23:37:43 2010 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Thu Feb 18 23:38:33 2010 +0100
     1.3 @@ -681,7 +681,7 @@
     1.4              |> def_pred abinding parms defs' exts exts';
     1.5            val (_, thy'') =
     1.6              thy'
     1.7 -            |> Sign.mandatory_path (Binding.name_of abinding)
     1.8 +            |> Sign.qualified_path true abinding
     1.9              |> PureThy.note_thmss ""
    1.10                [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.unfold_add])])]
    1.11              ||> Sign.restore_naming thy';
    1.12 @@ -695,7 +695,7 @@
    1.13              |> def_pred binding parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
    1.14            val (_, thy'''') =
    1.15              thy'''
    1.16 -            |> Sign.mandatory_path (Binding.name_of binding)
    1.17 +            |> Sign.qualified_path true binding
    1.18              |> PureThy.note_thmss ""
    1.19                   [((Binding.conceal (Binding.name introN), []), [([intro], [Locale.intro_add])]),
    1.20                    ((Binding.conceal (Binding.name axiomsN), []),