removed LocalTheory.target_naming/name;
authorwenzelm
Sat Nov 10 18:36:10 2007 +0100 (2007-11-10)
changeset 25381c100bf5bd6b8
parent 25380 03201004c77e
child 25382 72cfe89f7b21
removed LocalTheory.target_naming/name;
src/Pure/Isar/instance.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/Pure/Isar/instance.ML	Sat Nov 10 18:36:08 2007 +0100
     1.2 +++ b/src/Pure/Isar/instance.ML	Sat Nov 10 18:36:10 2007 +0100
     1.3 @@ -54,7 +54,6 @@
     1.4          type_syntax = LocalTheory.type_syntax,
     1.5          term_syntax = LocalTheory.term_syntax,
     1.6          declaration = LocalTheory.pretty,
     1.7 -        target_naming = LocalTheory.target_naming,
     1.8          reinit = LocalTheory.reinit,
     1.9          exit = LocalTheory.exit
    1.10        };
     2.1 --- a/src/Pure/Isar/local_theory.ML	Sat Nov 10 18:36:08 2007 +0100
     2.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Nov 10 18:36:10 2007 +0100
     2.3 @@ -37,8 +37,6 @@
     2.4      local_theory -> (bstring * thm list) * local_theory
     2.5    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     2.6    val target_morphism: local_theory -> morphism
     2.7 -  val target_naming: local_theory -> NameSpace.naming
     2.8 -  val target_name: local_theory -> bstring -> string
     2.9    val init: string -> operations -> Proof.context -> local_theory
    2.10    val restore: local_theory -> local_theory
    2.11    val reinit: local_theory -> local_theory
    2.12 @@ -66,7 +64,6 @@
    2.13    type_syntax: declaration -> local_theory -> local_theory,
    2.14    term_syntax: declaration -> local_theory -> local_theory,
    2.15    declaration: declaration -> local_theory -> local_theory,
    2.16 -  target_naming: local_theory -> NameSpace.naming,
    2.17    reinit: local_theory -> local_theory,
    2.18    exit: local_theory -> Proof.context};
    2.19  
    2.20 @@ -156,7 +153,6 @@
    2.21  val type_syntax = operation1 #type_syntax;
    2.22  val term_syntax = operation1 #term_syntax;
    2.23  val declaration = operation1 #declaration;
    2.24 -val target_naming = operation #target_naming;
    2.25  
    2.26  fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> the_single;
    2.27  
    2.28 @@ -168,8 +164,6 @@
    2.29    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    2.30    in term_syntax (ProofContext.target_notation add mode args) lthy end;
    2.31  
    2.32 -val target_name = NameSpace.full o target_naming;
    2.33 -
    2.34  
    2.35  (* init -- exit *)
    2.36  
     3.1 --- a/src/Pure/Isar/theory_target.ML	Sat Nov 10 18:36:08 2007 +0100
     3.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Nov 10 18:36:10 2007 +0100
     3.3 @@ -74,11 +74,6 @@
     3.4  val term_syntax = target_decl Locale.add_term_syntax;
     3.5  val declaration = target_decl Locale.add_declaration;
     3.6  
     3.7 -fun target_naming (Target {target, ...}) lthy =
     3.8 -  (if target = "" then Sign.naming_of (ProofContext.theory_of lthy)
     3.9 -   else ProofContext.naming_of (LocalTheory.target_of lthy))
    3.10 -  |> NameSpace.qualified_names;
    3.11 -
    3.12  fun class_target (Target {target, ...}) f =
    3.13    LocalTheory.raw_theory f #>
    3.14    LocalTheory.target (Class.refresh_syntax target);
    3.15 @@ -321,7 +316,6 @@
    3.16      type_syntax = type_syntax ta,
    3.17      term_syntax = term_syntax ta,
    3.18      declaration = declaration ta,
    3.19 -    target_naming = target_naming ta,
    3.20      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
    3.21      exit = LocalTheory.target_of}
    3.22  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;