provide direct access to the different kinds of type declarations;

--- a/src/Pure/sign.ML	Thu Feb 25 09:16:16 2010 +0100
+++ b/src/Pure/sign.ML	Thu Feb 25 22:05:34 2010 +0100
@@ -60,6 +60,7 @@
   val intern_term: theory -> term -> term
   val extern_term: theory -> term -> term
   val intern_tycons: theory -> typ -> typ
+  val the_type_decl: theory -> string -> Type.decl
   val arity_number: theory -> string -> int
   val arity_sorts: theory -> string -> sort -> sort list
   val certify_class: theory -> class -> class
@@ -308,6 +309,7 @@
 
 (* certify wrt. type signature *)
 
+val the_type_decl = Type.the_decl o tsig_of;
 val arity_number = Type.arity_number o tsig_of;
 fun arity_sorts thy = Type.arity_sorts (Syntax.pp_global thy) (tsig_of thy);
 

--- a/src/Pure/type.ML	Thu Feb 25 09:16:16 2010 +0100
+++ b/src/Pure/type.ML	Thu Feb 25 22:05:34 2010 +0100
@@ -35,6 +35,7 @@
   val get_mode: Proof.context -> mode
   val set_mode: mode -> Proof.context -> Proof.context
   val restore_mode: Proof.context -> Proof.context -> Proof.context
+  val the_decl: tsig -> string -> decl
   val cert_typ_mode: mode -> tsig -> typ -> typ
   val cert_typ: tsig -> typ -> typ
   val arity_number: tsig -> string -> int
@@ -163,6 +164,11 @@
 
 fun lookup_type (TSig {types = (_, types), ...}) = Symtab.lookup types;
 
+fun the_decl tsig c =
+  (case lookup_type tsig c of
+    NONE => error (undecl_type c)
+  | SOME decl => decl);
+
 
 (* certified types *)
 
@@ -189,15 +195,14 @@
             val Ts' = map cert Ts;
             fun nargs n = if length Ts <> n then err (bad_nargs c) else ();
           in
-            (case lookup_type tsig c of
-              SOME (LogicalType n) => (nargs n; Type (c, Ts'))
-            | SOME (Abbreviation (vs, U, syn)) =>
+            (case the_decl tsig c of
+              LogicalType n => (nargs n; Type (c, Ts'))
+            | Abbreviation (vs, U, syn) =>
                (nargs (length vs);
                 if syn then check_logical c else ();
                 if normalize then inst_typ (vs ~~ Ts') U
                 else Type (c, Ts'))
-            | SOME Nonterminal => (nargs 0; check_logical c; T)
-            | NONE => err (undecl_type c))
+            | Nonterminal => (nargs 0; check_logical c; T))
           end
       | cert (TFree (x, S)) = TFree (x, cert_sort tsig S)
       | cert (TVar (xi as (_, i), S)) =