src/Pure/Isar/proof_context.ML
changeset 42359 6ca5407863ed
parent 42358 b47d41d9f4b5
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -37,6 +37,15 @@
     1.4    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
     1.5    val facts_of: Proof.context -> Facts.T
     1.6    val cases_of: Proof.context -> (string * (Rule_Cases.T * bool)) list
     1.7 +  val class_space: Proof.context -> Name_Space.T
     1.8 +  val type_space: Proof.context -> Name_Space.T
     1.9 +  val const_space: Proof.context -> Name_Space.T
    1.10 +  val intern_class: Proof.context -> xstring -> string
    1.11 +  val intern_type: Proof.context -> xstring -> string
    1.12 +  val intern_const: Proof.context -> xstring -> string
    1.13 +  val extern_class: Proof.context -> string -> xstring
    1.14 +  val extern_type: Proof.context -> string -> xstring
    1.15 +  val extern_const: Proof.context -> string -> xstring
    1.16    val transfer_syntax: theory -> Proof.context -> Proof.context
    1.17    val transfer: theory -> Proof.context -> Proof.context
    1.18    val background_theory: (theory -> theory) -> Proof.context -> Proof.context
    1.19 @@ -269,6 +278,21 @@
    1.20  val cases_of = #cases o rep_context;
    1.21  
    1.22  
    1.23 +(* name spaces *)
    1.24 +
    1.25 +val class_space = Type.class_space o tsig_of;
    1.26 +val type_space = Type.type_space o tsig_of;
    1.27 +val const_space = Consts.space_of o consts_of;
    1.28 +
    1.29 +val intern_class = Name_Space.intern o class_space;
    1.30 +val intern_type = Name_Space.intern o type_space;
    1.31 +val intern_const = Name_Space.intern o const_space;
    1.32 +
    1.33 +fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
    1.34 +fun extern_type ctxt = Name_Space.extern ctxt (type_space ctxt);
    1.35 +fun extern_const ctxt = Name_Space.extern ctxt (const_space ctxt);
    1.36 +
    1.37 +
    1.38  (* theory transfer *)
    1.39  
    1.40  fun transfer_syntax thy ctxt = ctxt |>
    1.41 @@ -351,7 +375,7 @@
    1.42  
    1.43  in
    1.44  
    1.45 -val read_arity = prep_arity (Type.intern_type o tsig_of) Syntax.read_sort;
    1.46 +val read_arity = prep_arity intern_type Syntax.read_sort;
    1.47  val cert_arity = prep_arity (K I) (Type.cert_sort o tsig_of);
    1.48  
    1.49  end;
    1.50 @@ -452,7 +476,7 @@
    1.51        TFree (c, default_sort ctxt (c, ~1)))
    1.52      else
    1.53        let
    1.54 -        val d = Type.intern_type tsig c;
    1.55 +        val d = intern_type ctxt c;
    1.56          val decl = Type.the_decl tsig d;
    1.57          val _ = Context_Position.report ctxt pos (Markup.tycon d);
    1.58          fun err () = error ("Bad type name: " ^ quote d);