src/Pure/Isar/theory_target.ML
changeset 25381 c100bf5bd6b8
parent 25372 a718f1ccaf1a
child 25392 bb8d225dcf05
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sat Nov 10 18:36:08 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Nov 10 18:36:10 2007 +0100
     1.3 @@ -74,11 +74,6 @@
     1.4  val term_syntax = target_decl Locale.add_term_syntax;
     1.5  val declaration = target_decl Locale.add_declaration;
     1.6  
     1.7 -fun target_naming (Target {target, ...}) lthy =
     1.8 -  (if target = "" then Sign.naming_of (ProofContext.theory_of lthy)
     1.9 -   else ProofContext.naming_of (LocalTheory.target_of lthy))
    1.10 -  |> NameSpace.qualified_names;
    1.11 -
    1.12  fun class_target (Target {target, ...}) f =
    1.13    LocalTheory.raw_theory f #>
    1.14    LocalTheory.target (Class.refresh_syntax target);
    1.15 @@ -321,7 +316,6 @@
    1.16      type_syntax = type_syntax ta,
    1.17      term_syntax = term_syntax ta,
    1.18      declaration = declaration ta,
    1.19 -    target_naming = target_naming ta,
    1.20      reinit = fn lthy => init_lthy_ctxt ta (ProofContext.theory_of lthy),
    1.21      exit = LocalTheory.target_of}
    1.22  and init_lthy_ctxt ta = init_lthy ta o init_ctxt ta;