removed obsolete no_base_names;
authorwenzelm
Tue, 10 Mar 2009 21:19:22 +0100
changeset 30420 ebbec8d8d7a9
parent 30419 c944e299eaf9
child 30421 9498e99e58a6
removed obsolete no_base_names; tuned;
src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Tue Mar 10 21:18:52 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 10 21:19:22 2009 +0100
@@ -97,9 +97,8 @@
   val get_thms: Proof.context -> xstring -> thm list
   val get_thm: Proof.context -> xstring -> thm
   val add_path: string -> Proof.context -> Proof.context
-  val no_base_names: Proof.context -> Proof.context
+  val sticky_prefix: string -> Proof.context -> Proof.context
   val qualified_names: Proof.context -> Proof.context
-  val sticky_prefix: 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,9 +944,8 @@
 (* name space operations *)
 
 val add_path        = map_naming o NameSpace.add_path;
-val no_base_names   = map_naming NameSpace.no_base_names;
+val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val qualified_names = map_naming NameSpace.qualified_names;
-val sticky_prefix   = map_naming o NameSpace.sticky_prefix;
 val restore_naming  = map_naming o K o naming_of;
 val reset_naming    = map_naming (K local_naming);