# HG changeset patch
# User wenzelm
# Date 1194716170 -3600
# Node ID c100bf5bd6b8a9e5bb7f07a80db081ad8490ca94
# Parent  03201004c77e7026ca13b5d068309a7541a080ca
removed LocalTheory.target_naming/name;

diff -r 03201004c77e -r c100bf5bd6b8 src/Pure/Isar/instance.ML
--- a/src/Pure/Isar/instance.ML	Sat Nov 10 18:36:08 2007 +0100
+++ b/src/Pure/Isar/instance.ML	Sat Nov 10 18:36:10 2007 +0100
@@ -54,7 +54,6 @@
         type_syntax = LocalTheory.type_syntax,
         term_syntax = LocalTheory.term_syntax,
         declaration = LocalTheory.pretty,
-        target_naming = LocalTheory.target_naming,
         reinit = LocalTheory.reinit,
         exit = LocalTheory.exit
       };
diff -r 03201004c77e -r c100bf5bd6b8 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sat Nov 10 18:36:08 2007 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sat Nov 10 18:36:10 2007 +0100
@@ -37,8 +37,6 @@
     local_theory -> (bstring * thm list) * local_theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
   val target_morphism: local_theory -> morphism
-  val target_naming: local_theory -> NameSpace.naming
-  val target_name: local_theory -> bstring -> string
   val init: string -> operations -> Proof.context -> local_theory
   val restore: local_theory -> local_theory
   val reinit: local_theory -> local_theory
@@ -66,7 +64,6 @@
   type_syntax: declaration -> local_theory -> local_theory,
   term_syntax: declaration -> local_theory -> local_theory,
   declaration: declaration -> local_theory -> local_theory,
-  target_naming: local_theory -> NameSpace.naming,
   reinit: local_theory -> local_theory,
   exit: local_theory -> Proof.context};
 
@@ -156,7 +153,6 @@
 val type_syntax = operation1 #type_syntax;
 val term_syntax = operation1 #term_syntax;
 val declaration = operation1 #declaration;
-val target_naming = operation #target_naming;
 
 fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> the_single;
 
@@ -168,8 +164,6 @@
   let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   in term_syntax (ProofContext.target_notation add mode args) lthy end;
 
-val target_name = NameSpace.full o target_naming;
-
 
 (* init -- exit *)
 
diff -r 03201004c77e -r c100bf5bd6b8 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sat Nov 10 18:36:08 2007 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sat Nov 10 18:36:10 2007 +0100
@@ -74,11 +74,6 @@
 val term_syntax = target_decl Locale.add_term_syntax;
 val declaration = target_decl Locale.add_declaration;
 
-fun target_naming (Target {target, ...}) lthy =
-  (if target = "" then Sign.naming_of (ProofContext.theory_of lthy)
-   else ProofContext.naming_of (LocalTheory.target_of lthy))
-  |> NameSpace.qualified_names;
-
 fun class_target (Target {target, ...}) f =
   LocalTheory.raw_theory f #>
   LocalTheory.target (Class.refresh_syntax target);
@@ -321,7 +316,6 @@
     type_syntax = type_syntax ta,
     term_syntax = term_syntax ta,
     declaration = declaration ta,
-    target_naming = target_naming ta,
     reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
     exit = LocalTheory.target_of}
 and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;