--- a/src/Pure/Isar/expression.ML Thu Mar 12 11:17:34 2009 +0100
+++ b/src/Pure/Isar/expression.ML Thu Mar 12 12:04:27 2009 +0100
@@ -674,8 +674,7 @@
|> def_pred aname parms defs' exts exts';
val (_, thy'') =
thy'
- |> Sign.add_path (Binding.name_of aname)
- |> Sign.no_base_names
+ |> Sign.sticky_prefix (Binding.name_of aname)
|> PureThy.note_thmss Thm.internalK
[((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])]
||> Sign.restore_naming thy';
@@ -689,8 +688,7 @@
|> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
val (_, thy'''') =
thy'''
- |> Sign.add_path (Binding.name_of pname)
- |> Sign.no_base_names
+ |> Sign.sticky_prefix (Binding.name_of pname)
|> PureThy.note_thmss Thm.internalK
[((Binding.name introN, []), [([intro], [Locale.intro_attrib])]),
((Binding.name axiomsN, []),