renamed sticky_prefix to mandatory_path;
authorwenzelm
Thu Mar 12 13:18:42 2009 +0100 (2009-03-12)
changeset 30469de9e8f1d927c
parent 30468 0cf8f536ef98
child 30470 9ae8f9d78cd3
child 30475 03765a88f652
renamed sticky_prefix to mandatory_path;
src/Pure/General/name_space.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/proof_context.ML
src/Pure/axclass.ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/General/name_space.ML	Thu Mar 12 12:04:27 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Mar 12 13:18:42 2009 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4    val root_path: naming -> naming
     1.5    val parent_path: naming -> naming
     1.6    val no_base_names: naming -> naming
     1.7 -  val sticky_prefix: string -> naming -> naming
     1.8 +  val mandatory_path: string -> naming -> naming
     1.9    type 'a table = T * 'a Symtab.table
    1.10    val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
    1.11    val empty_table: 'a table
    1.12 @@ -194,7 +194,7 @@
    1.13  val parent_path = map_naming (fn (path, no_base_names) =>
    1.14    (perhaps (try (#1 o split_last)) path, no_base_names));
    1.15  
    1.16 -fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
    1.17 +fun mandatory_path elems = map_naming (fn (path, no_base_names) =>
    1.18    (path @ [(elems, true)], no_base_names));
    1.19  
    1.20  val no_base_names = map_naming (fn (path, _) => (path, true));
     2.1 --- a/src/Pure/Isar/expression.ML	Thu Mar 12 12:04:27 2009 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Thu Mar 12 13:18:42 2009 +0100
     2.3 @@ -674,7 +674,7 @@
     2.4              |> def_pred aname parms defs' exts exts';
     2.5            val (_, thy'') =
     2.6              thy'
     2.7 -            |> Sign.sticky_prefix (Binding.name_of aname)
     2.8 +            |> Sign.mandatory_path (Binding.name_of aname)
     2.9              |> PureThy.note_thmss Thm.internalK
    2.10                [((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])]
    2.11              ||> Sign.restore_naming thy';
    2.12 @@ -688,7 +688,7 @@
    2.13              |> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
    2.14            val (_, thy'''') =
    2.15              thy'''
    2.16 -            |> Sign.sticky_prefix (Binding.name_of pname)
    2.17 +            |> Sign.mandatory_path (Binding.name_of pname)
    2.18              |> PureThy.note_thmss Thm.internalK
    2.19                   [((Binding.name introN, []), [([intro], [Locale.intro_attrib])]),
    2.20                    ((Binding.name axiomsN, []),
     3.1 --- a/src/Pure/Isar/local_theory.ML	Thu Mar 12 12:04:27 2009 +0100
     3.2 +++ b/src/Pure/Isar/local_theory.ML	Thu Mar 12 13:18:42 2009 +0100
     3.3 @@ -138,12 +138,12 @@
     3.4  
     3.5  fun full_naming lthy =
     3.6    Sign.naming_of (ProofContext.theory_of lthy)
     3.7 -  |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
     3.8 +  |> NameSpace.mandatory_path (#theory_prefix (get_lthy lthy));
     3.9  
    3.10  fun full_name naming = NameSpace.full_name (full_naming naming);
    3.11  
    3.12  fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
    3.13 -  |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
    3.14 +  |> Sign.mandatory_path (#theory_prefix (get_lthy lthy))
    3.15    |> f
    3.16    ||> Sign.restore_naming thy);
    3.17  
     4.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 12 12:04:27 2009 +0100
     4.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 12 13:18:42 2009 +0100
     4.3 @@ -97,7 +97,7 @@
     4.4    val get_thms: Proof.context -> xstring -> thm list
     4.5    val get_thm: Proof.context -> xstring -> thm
     4.6    val add_path: string -> Proof.context -> Proof.context
     4.7 -  val sticky_prefix: string -> Proof.context -> Proof.context
     4.8 +  val mandatory_path: string -> Proof.context -> Proof.context
     4.9    val restore_naming: Proof.context -> Proof.context -> Proof.context
    4.10    val reset_naming: Proof.context -> Proof.context
    4.11    val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
    4.12 @@ -945,7 +945,7 @@
    4.13  (* name space operations *)
    4.14  
    4.15  val add_path        = map_naming o NameSpace.add_path;
    4.16 -val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    4.17 +val mandatory_path  = map_naming o NameSpace.mandatory_path;
    4.18  val restore_naming  = map_naming o K o naming_of;
    4.19  val reset_naming    = map_naming (K local_naming);
    4.20  
     5.1 --- a/src/Pure/axclass.ML	Thu Mar 12 12:04:27 2009 +0100
     5.2 +++ b/src/Pure/axclass.ML	Thu Mar 12 13:18:42 2009 +0100
     5.3 @@ -370,7 +370,7 @@
     5.4      val T' = Type.strip_sorts T;
     5.5    in
     5.6      thy
     5.7 -    |> Sign.sticky_prefix name_inst
     5.8 +    |> Sign.mandatory_path name_inst
     5.9      |> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
    5.10      |-> (fn const' as Const (c'', _) =>
    5.11        Thm.add_def false true
    5.12 @@ -480,7 +480,7 @@
    5.13      val class_triv = Thm.class_triv def_thy class;
    5.14      val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
    5.15        def_thy
    5.16 -      |> Sign.sticky_prefix (Binding.name_of bconst)
    5.17 +      |> Sign.mandatory_path (Binding.name_of bconst)
    5.18        |> PureThy.note_thmss ""
    5.19          [((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
    5.20           ((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),
     6.1 --- a/src/Pure/sign.ML	Thu Mar 12 12:04:27 2009 +0100
     6.2 +++ b/src/Pure/sign.ML	Thu Mar 12 13:18:42 2009 +0100
     6.3 @@ -124,7 +124,7 @@
     6.4    val add_path: string -> theory -> theory
     6.5    val root_path: theory -> theory
     6.6    val parent_path: theory -> theory
     6.7 -  val sticky_prefix: string -> theory -> theory
     6.8 +  val mandatory_path: string -> theory -> theory
     6.9    val no_base_names: theory -> theory
    6.10    val local_path: theory -> theory
    6.11    val restore_naming: theory -> theory -> theory
    6.12 @@ -619,7 +619,7 @@
    6.13  val add_path        = map_naming o NameSpace.add_path;
    6.14  val root_path       = map_naming NameSpace.root_path;
    6.15  val parent_path     = map_naming NameSpace.parent_path;
    6.16 -val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    6.17 +val mandatory_path  = map_naming o NameSpace.mandatory_path;
    6.18  val no_base_names   = map_naming NameSpace.no_base_names;
    6.19  
    6.20  fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);