src/Pure/Isar/local_theory.ML
changeset 25381 c100bf5bd6b8
parent 25289 3d332d8a827c
child 25984 da0399c9ffcb
     1.1 --- a/src/Pure/Isar/local_theory.ML	Sat Nov 10 18:36:08 2007 +0100
     1.2 +++ b/src/Pure/Isar/local_theory.ML	Sat Nov 10 18:36:10 2007 +0100
     1.3 @@ -37,8 +37,6 @@
     1.4      local_theory -> (bstring * thm list) * local_theory
     1.5    val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
     1.6    val target_morphism: local_theory -> morphism
     1.7 -  val target_naming: local_theory -> NameSpace.naming
     1.8 -  val target_name: local_theory -> bstring -> string
     1.9    val init: string -> operations -> Proof.context -> local_theory
    1.10    val restore: local_theory -> local_theory
    1.11    val reinit: local_theory -> local_theory
    1.12 @@ -66,7 +64,6 @@
    1.13    type_syntax: declaration -> local_theory -> local_theory,
    1.14    term_syntax: declaration -> local_theory -> local_theory,
    1.15    declaration: declaration -> local_theory -> local_theory,
    1.16 -  target_naming: local_theory -> NameSpace.naming,
    1.17    reinit: local_theory -> local_theory,
    1.18    exit: local_theory -> Proof.context};
    1.19  
    1.20 @@ -156,7 +153,6 @@
    1.21  val type_syntax = operation1 #type_syntax;
    1.22  val term_syntax = operation1 #term_syntax;
    1.23  val declaration = operation1 #declaration;
    1.24 -val target_naming = operation #target_naming;
    1.25  
    1.26  fun note kind (a, ths) lthy = lthy |> notes kind [(a, [(ths, [])])] |>> the_single;
    1.27  
    1.28 @@ -168,8 +164,6 @@
    1.29    let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
    1.30    in term_syntax (ProofContext.target_notation add mode args) lthy end;
    1.31  
    1.32 -val target_name = NameSpace.full o target_naming;
    1.33 -
    1.34  
    1.35  (* init -- exit *)
    1.36