added declare_typ;

--- a/src/Pure/variable.ML	Thu Jun 19 20:48:03 2008 +0200
+++ b/src/Pure/variable.ML	Thu Jun 19 20:48:04 2008 +0200
@@ -22,10 +22,10 @@
   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
@@ -222,6 +222,8 @@
   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;