renamed sticky_prefix to mandatory_path;

--- a/src/Pure/General/name_space.ML	Thu Mar 12 12:04:27 2009 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 12 13:18:42 2009 +0100
@@ -36,7 +36,7 @@
   val root_path: naming -> naming
   val parent_path: naming -> naming
   val no_base_names: naming -> naming
-  val sticky_prefix: string -> naming -> naming
+  val mandatory_path: string -> naming -> naming
   type 'a table = T * 'a Symtab.table
   val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
   val empty_table: 'a table
@@ -194,7 +194,7 @@
 val parent_path = map_naming (fn (path, no_base_names) =>
   (perhaps (try (#1 o split_last)) path, no_base_names));
 
-fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
+fun mandatory_path elems = map_naming (fn (path, no_base_names) =>
   (path @ [(elems, true)], no_base_names));
 
 val no_base_names = map_naming (fn (path, _) => (path, true));

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

--- a/src/Pure/Isar/local_theory.ML	Thu Mar 12 12:04:27 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Thu Mar 12 13:18:42 2009 +0100
@@ -138,12 +138,12 @@
 
 fun full_naming lthy =
   Sign.naming_of (ProofContext.theory_of lthy)
-  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
+  |> NameSpace.mandatory_path (#theory_prefix (get_lthy lthy));
 
 fun full_name naming = NameSpace.full_name (full_naming naming);
 
 fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
-  |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
+  |> Sign.mandatory_path (#theory_prefix (get_lthy lthy))
   |> f
   ||> Sign.restore_naming thy);
 

--- a/src/Pure/Isar/proof_context.ML	Thu Mar 12 12:04:27 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Mar 12 13:18:42 2009 +0100
@@ -97,7 +97,7 @@
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
   val add_path: string -> Proof.context -> Proof.context
-  val sticky_prefix: string -> Proof.context -> Proof.context
+  val mandatory_path: string -> Proof.context -> Proof.context
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val reset_naming: Proof.context -> Proof.context
   val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
@@ -945,7 +945,7 @@
 (* name space operations *)
 
 val add_path        = map_naming o NameSpace.add_path;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
+val mandatory_path  = map_naming o NameSpace.mandatory_path;
 val restore_naming  = map_naming o K o naming_of;
 val reset_naming    = map_naming (K local_naming);
 

--- a/src/Pure/axclass.ML	Thu Mar 12 12:04:27 2009 +0100
+++ b/src/Pure/axclass.ML	Thu Mar 12 13:18:42 2009 +0100
@@ -370,7 +370,7 @@
     val T' = Type.strip_sorts T;
   in
     thy
-    |> Sign.sticky_prefix name_inst
+    |> Sign.mandatory_path name_inst
     |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
     |-> (fn const' as Const (c'', _) =>
       Thm.add_def false true
@@ -480,7 +480,7 @@
     val class_triv = Thm.class_triv def_thy class;
     val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
       def_thy
-      |> Sign.sticky_prefix (Binding.name_of bconst)
+      |> Sign.mandatory_path (Binding.name_of bconst)
       |> PureThy.note_thmss ""
         [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
          ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),

--- a/src/Pure/sign.ML	Thu Mar 12 12:04:27 2009 +0100
+++ b/src/Pure/sign.ML	Thu Mar 12 13:18:42 2009 +0100
@@ -124,7 +124,7 @@
   val add_path: string -> theory -> theory
   val root_path: theory -> theory
   val parent_path: theory -> theory
-  val sticky_prefix: string -> theory -> theory
+  val mandatory_path: string -> theory -> theory
   val no_base_names: theory -> theory
   val local_path: theory -> theory
   val restore_naming: theory -> theory -> theory
@@ -619,7 +619,7 @@
 val add_path        = map_naming o NameSpace.add_path;
 val root_path       = map_naming NameSpace.root_path;
 val parent_path     = map_naming NameSpace.parent_path;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
+val mandatory_path  = map_naming o NameSpace.mandatory_path;
 val no_base_names   = map_naming NameSpace.no_base_names;
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);