src/Pure/Isar/expression.ML

           val ((statement, intro, axioms), thy') =
             thy
             |> 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';
           in (SOME statement, SOME intro, axioms, thy'') end;
     val (b_pred, b_intro, b_axioms, thy'''') =

           val ((statement, intro, axioms), thy''') =
             thy''
             |> 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, []),
                     [(map (Drule.standard o Element.conclude_witness) axioms, [])])]
             ||> Sign.restore_naming thy''';