src/Pure/Isar/proof_context.ML
changeset 61261 ddb2da7cb2e4
parent 61168 dcdfb6355a05
child 61262 7bd1eb4b056e
equal deleted inserted replaced
61260:e6f03fae14d5 61261:ddb2da7cb2e4
    42   val qualified: Position.T -> Proof.context -> Proof.context
    42   val qualified: Position.T -> Proof.context -> Proof.context
    43   val concealed: Proof.context -> Proof.context
    43   val concealed: Proof.context -> Proof.context
    44   val class_space: Proof.context -> Name_Space.T
    44   val class_space: Proof.context -> Name_Space.T
    45   val type_space: Proof.context -> Name_Space.T
    45   val type_space: Proof.context -> Name_Space.T
    46   val const_space: Proof.context -> Name_Space.T
    46   val const_space: Proof.context -> Name_Space.T
       
    47   val defs_context: Proof.context -> Defs.context
    47   val intern_class: Proof.context -> xstring -> string
    48   val intern_class: Proof.context -> xstring -> string
    48   val intern_type: Proof.context -> xstring -> string
    49   val intern_type: Proof.context -> xstring -> string
    49   val intern_const: Proof.context -> xstring -> string
    50   val intern_const: Proof.context -> xstring -> string
    50   val extern_class: Proof.context -> string -> xstring
    51   val extern_class: Proof.context -> string -> xstring
    51   val markup_class: Proof.context -> string -> string
    52   val markup_class: Proof.context -> string -> string
   320 
   321 
   321 val class_space = Type.class_space o tsig_of;
   322 val class_space = Type.class_space o tsig_of;
   322 val type_space = Type.type_space o tsig_of;
   323 val type_space = Type.type_space o tsig_of;
   323 val const_space = Consts.space_of o consts_of;
   324 val const_space = Consts.space_of o consts_of;
   324 
   325 
       
   326 fun defs_context ctxt = (ctxt, SOME (const_space ctxt, type_space ctxt));
       
   327 
   325 val intern_class = Name_Space.intern o class_space;
   328 val intern_class = Name_Space.intern o class_space;
   326 val intern_type = Name_Space.intern o type_space;
   329 val intern_type = Name_Space.intern o type_space;
   327 val intern_const = Name_Space.intern o const_space;
   330 val intern_const = Name_Space.intern o const_space;
   328 
   331 
   329 fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);
   332 fun extern_class ctxt = Name_Space.extern ctxt (class_space ctxt);