src/Pure/variable.ML

   val newly_fixed: Proof.context -> Proof.context -> string -> bool
   val add_fixed: Proof.context -> term -> (string * typ) list -> (string * typ) list
   val default_type: Proof.context -> string -> typ option
   val def_type: Proof.context -> bool -> indexname -> typ option
   val def_sort: Proof.context -> indexname -> sort option
+  val declare_names: term -> Proof.context -> Proof.context
   val declare_constraints: term -> Proof.context -> Proof.context
-  val declare_names: term -> Proof.context -> Proof.context
-  val declare_internal: term -> Proof.context -> Proof.context
   val declare_term: term -> Proof.context -> Proof.context
+  val declare_typ: typ -> Proof.context -> Proof.context
   val declare_prf: Proofterm.proof -> Proof.context -> Proof.context
   val declare_thm: thm -> Proof.context -> Proof.context
   val thm_context: thm -> Proof.context
   val variant_frees: Proof.context -> term list -> (string * 'a) list -> (string * 'a) list
   val add_binds: (indexname * term option) list -> Proof.context -> Proof.context

 
 fun declare_term t =
   declare_internal t #>
   declare_constraints t;
 
+val declare_typ = declare_term o Logic.mk_type;
+
 val declare_prf = Proofterm.fold_proof_terms declare_internal (declare_internal o Logic.mk_type);
 
 val declare_thm = Thm.fold_terms declare_internal;
 fun thm_context th = declare_thm th (ProofContext.init (Thm.theory_of_thm th));