src/Pure/Isar/proof_context.ML
changeset 30469 de9e8f1d927c
parent 30438 c2d49315b93b
child 30473 e0b66c11e7e4
     1.1 --- a/src/Pure/Isar/proof_context.ML	Thu Mar 12 12:04:27 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Mar 12 13:18:42 2009 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4    val get_thms: Proof.context -> xstring -> thm list
     1.5    val get_thm: Proof.context -> xstring -> thm
     1.6    val add_path: string -> Proof.context -> Proof.context
     1.7 -  val sticky_prefix: string -> Proof.context -> Proof.context
     1.8 +  val mandatory_path: string -> Proof.context -> Proof.context
     1.9    val restore_naming: Proof.context -> Proof.context -> Proof.context
    1.10    val reset_naming: Proof.context -> Proof.context
    1.11    val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
    1.12 @@ -945,7 +945,7 @@
    1.13  (* name space operations *)
    1.14  
    1.15  val add_path        = map_naming o NameSpace.add_path;
    1.16 -val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
    1.17 +val mandatory_path  = map_naming o NameSpace.mandatory_path;
    1.18  val restore_naming  = map_naming o K o naming_of;
    1.19  val reset_naming    = map_naming (K local_naming);
    1.20