Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
locale: more precise treatment of naming vs. binding;
authorwenzelm
Thu, 18 Feb 2010 23:38:33 +0100
changeset 35204 214ec053128e
parent 35203 ef65a2218c31
child 35205 611b90bb89bc
locale: more precise treatment of naming vs. binding;
src/Pure/Isar/expression.ML file | annotate | diff | comparison | revisions 
--- 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), []),
isabelle