src/Pure/Isar/proof_context.ML

   val naming_of: Proof.context -> Name_Space.naming
   val restore_naming: Proof.context -> Proof.context -> Proof.context
   val full_name: Proof.context -> binding -> string
   val syn_of: Proof.context -> Syntax.syntax
   val tsig_of: Proof.context -> Type.tsig
+  val set_defsort: sort -> Proof.context -> Proof.context
   val default_sort: Proof.context -> indexname -> sort
   val consts_of: Proof.context -> Consts.T
   val the_const_constraint: Proof.context -> string -> typ
   val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
   val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context

 
 (** Isar proof context information **)
 
 datatype ctxt =
   Ctxt of
-   {mode: mode,                       (*inner syntax mode*)
-    naming: Name_Space.naming,        (*local naming conventions*)
-    syntax: Local_Syntax.T,           (*local syntax*)
-    tsig: Type.tsig * Type.tsig,      (*local/global type signature -- local name space only*)
-    consts: Consts.T * Consts.T,      (*local/global consts -- local name space/abbrevs only*)
-    facts: Facts.T,                   (*local facts*)
+   {mode: mode,                  (*inner syntax mode*)
+    naming: Name_Space.naming,   (*local naming conventions*)
+    syntax: Local_Syntax.T,      (*local syntax*)
+    tsig: Type.tsig * Type.tsig, (*local/global type signature -- local name space / defsort only*)
+    consts: Consts.T * Consts.T, (*local/global consts -- local name space / abbrevs only*)
+    facts: Facts.T,              (*local facts*)
     cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
 
 fun make_ctxt (mode, naming, syntax, tsig, consts, facts, cases) =
   Ctxt {mode = mode, naming = naming, syntax = syntax,
     tsig = tsig, consts = consts, facts = facts, cases = cases};

 val syn_of = Local_Syntax.syn_of o syntax_of;
 val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
 val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
 
 val tsig_of = #1 o #tsig o rep_context;
+val set_defsort = map_tsig o apfst o Type.set_defsort;
 fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
 
 val consts_of = #1 o #consts o rep_context;
 val the_const_constraint = Consts.the_constraint o consts_of;