--- 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);