# HG changeset patch
# User wenzelm
# Date 1236855867 -3600
# Node ID 0cf8f536ef98c091426e4945bd29e5d799f1ae25
# Parent  afd0e5095c6ba5c3d344a40e414d626e865528b1
replaced old-style add_path/no_base_names by sticky_prefix;

diff -r afd0e5095c6b -r 0cf8f536ef98 src/Pure/Isar/expression.ML
--- 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, []),
diff -r afd0e5095c6b -r 0cf8f536ef98 src/Pure/axclass.ML
--- a/src/Pure/axclass.ML	Thu Mar 12 11:17:34 2009 +0100
+++ b/src/Pure/axclass.ML	Thu Mar 12 12:04:27 2009 +0100
@@ -371,7 +371,6 @@
   in
     thy
     |> Sign.sticky_prefix name_inst
-    |> Sign.no_base_names
     |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
     |-> (fn const' as Const (c'', _) =>
       Thm.add_def false true
@@ -481,8 +480,7 @@
     val class_triv = Thm.class_triv def_thy class;
     val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
       def_thy
-      |> Sign.add_path (Binding.name_of bconst)
-      |> Sign.no_base_names
+      |> Sign.sticky_prefix (Binding.name_of bconst)
       |> PureThy.note_thmss ""
         [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
          ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),