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