# HG changeset patch
# User wenzelm
# Date 1236716362 -3600
# Node ID ebbec8d8d7a9aa2b89bc23f70fac2198507b74a2
# Parent  c944e299eaf90d39baed555f78f9dff89dfe927c
removed obsolete no_base_names;
tuned;

diff -r c944e299eaf9 -r ebbec8d8d7a9 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);