src/Pure/Isar/proof_context.ML
changeset 36451 ddc965e172c4
parent 36450 62eaaffe6e47
child 36503 bd4e2821482a
     1.1 --- a/src/Pure/Isar/proof_context.ML	Wed Apr 28 11:13:11 2010 +0200
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Wed Apr 28 11:41:27 2010 +0200
     1.3 @@ -28,6 +28,7 @@
     1.4    val full_name: Proof.context -> binding -> string
     1.5    val syn_of: Proof.context -> Syntax.syntax
     1.6    val tsig_of: Proof.context -> Type.tsig
     1.7 +  val set_defsort: sort -> Proof.context -> Proof.context
     1.8    val default_sort: Proof.context -> indexname -> sort
     1.9    val consts_of: Proof.context -> Consts.T
    1.10    val the_const_constraint: Proof.context -> string -> typ
    1.11 @@ -178,12 +179,12 @@
    1.12  
    1.13  datatype ctxt =
    1.14    Ctxt of
    1.15 -   {mode: mode,                       (*inner syntax mode*)
    1.16 -    naming: Name_Space.naming,        (*local naming conventions*)
    1.17 -    syntax: Local_Syntax.T,           (*local syntax*)
    1.18 -    tsig: Type.tsig * Type.tsig,      (*local/global type signature -- local name space only*)
    1.19 -    consts: Consts.T * Consts.T,      (*local/global consts -- local name space/abbrevs only*)
    1.20 -    facts: Facts.T,                   (*local facts*)
    1.21 +   {mode: mode,                  (*inner syntax mode*)
    1.22 +    naming: Name_Space.naming,   (*local naming conventions*)
    1.23 +    syntax: Local_Syntax.T,      (*local syntax*)
    1.24 +    tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
    1.25 +    consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
    1.26 +    facts: Facts.T,              (*local facts*)
    1.27      cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    1.28  
    1.29  fun make_ctxt (mode, naming, syntax, tsig, consts, facts, cases) =
    1.30 @@ -255,6 +256,7 @@
    1.31  val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
    1.32  
    1.33  val tsig_of = #1 o #tsig o rep_context;
    1.34 +val set_defsort = map_tsig o apfst o Type.set_defsort;
    1.35  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
    1.36  
    1.37  val consts_of = #1 o #consts o rep_context;