src/Pure/Isar/code.ML

   val subst_signatures: theory -> term -> term
   val args_number: theory -> string -> int
 
   (*constructor sets*)
   val constrset_of_consts: theory -> (string * typ) list
-    -> string * ((string * sort) list * (string * typ list) list)
+    -> string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
 
   (*code equations and certificates*)
   val mk_eqn: theory -> thm * bool -> thm * bool
   val mk_eqn_warning: theory -> thm -> (thm * bool) option
   val mk_eqn_liberal: theory -> thm -> (thm * bool) option

   val add_signature: string * typ -> theory -> theory
   val add_signature_cmd: string * string -> theory -> theory
   val add_datatype: (string * typ) list -> theory -> theory
   val add_datatype_cmd: string list -> theory -> theory
   val datatype_interpretation:
-    (string * ((string * sort) list * (string * typ list) list)
+    (string * ((string * sort) list * (string * ((string * sort) list * typ list)) list)
       -> theory -> theory) -> theory -> theory
   val add_abstype: thm -> theory -> theory
   val abstype_interpretation:
-    (string * ((string * sort) list * ((string * typ) * (string * thm)))
+    (string * ((string * sort) list * ((string * ((string * sort) list * typ)) * (string * thm)))
       -> theory -> theory) -> theory -> theory
   val add_eqn: thm -> theory -> theory
   val add_nbe_eqn: thm -> theory -> theory
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute

   val add_nbe_default_eqn_attrib: Attrib.src
   val del_eqn: thm -> theory -> theory
   val del_eqns: string -> theory -> theory
   val add_case: thm -> theory -> theory
   val add_undefined: string -> theory -> theory
-  val get_type: theory -> string -> ((string * sort) list * ((string * string list) * typ list) list)
+  val get_type: theory -> string
+    -> ((string * sort) list * (string * ((string * sort) list * typ list)) list) * bool
   val get_type_of_constr_or_abstr: theory -> string -> (string * bool) option
   val is_constr: theory -> string -> bool
   val is_abstr: theory -> string -> bool
   val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
   val get_case_scheme: theory -> string -> (int * (int * string list)) option

 
 (** data store **)
 
 (* datatypes *)
 
-datatype typ_spec = Constructors of (string * typ list) list
-  | Abstractor of (string * typ) * (string * thm);
+datatype typ_spec = Constructors of (string * ((string * sort) list * typ list)) list
+  | Abstractor of (string * ((string * sort) list * typ)) * (string * thm);
 
 fun constructors_of (Constructors cos) = (cos, false)
-  | constructors_of (Abstractor ((co, ty), _)) = ([(co, [ty])], true);
+  | constructors_of (Abstractor ((co, (vs, ty)), _)) = ([(co, (vs, [ty]))], true);
 
 
 (* functions *)
 
 datatype fun_spec = Default of (thm * bool) list * (thm * bool) list lazy

       in ((tyco, sorts), c :: cs) end;
     fun inst vs' (c, (vs, ty)) =
       let
         val the_v = the o AList.lookup (op =) (vs ~~ vs');
         val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
-      in (c, (fst o strip_type) ty') end;
+        val vs'' = map dest_TFree (Sign.const_typargs thy (c, ty'));
+      in (c, (vs'', (fst o strip_type) ty')) end;
     val c' :: cs' = map (ty_sorts thy) cs;
     val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
     val vs = Name.names Name.context Name.aT sorts;
     val cs''' = map (inst vs) cs'';
   in (tyco, (vs, rev cs''')) end;
 
 fun get_type_entry thy tyco = case these (Symtab.lookup ((the_types o the_exec) thy) tyco)
  of (_, entry) :: _ => SOME entry
   | _ => NONE;
 
-fun get_type_spec thy tyco = case get_type_entry thy tyco
+fun get_type thy tyco = case get_type_entry thy tyco
  of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
   | NONE => arity_number thy tyco
       |> Name.invents Name.context Name.aT
       |> map (rpair [])
       |> rpair []

 
 fun get_abstype_spec thy tyco = case get_type_entry thy tyco
  of SOME (vs, Abstractor spec) => (vs, spec)
   | _ => error ("Not an abstract type: " ^ tyco);
  
-fun get_type thy tyco =
-  let
-    val ((vs, cos), _) = get_type_spec thy tyco;
-    fun args_of c tys = map (fst o dest_TFree)
-      (Sign.const_typargs thy (c, tys ---> Type (tyco, map TFree vs)));
-    fun add_typargs (c, tys) = ((c, args_of c tys), tys);
-  in (vs, map add_typargs cos) end;
-
 fun get_type_of_constr_or_abstr thy c =
   case (snd o strip_type o const_typ thy) c
-   of Type (tyco, _) => let val ((vs, cos), abstract) = get_type_spec thy tyco
+   of Type (tyco, _) => let val ((vs, cos), abstract) = get_type thy tyco
         in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
     | _ => NONE;
 
 fun is_constr thy c = case get_type_of_constr_or_abstr thy c
  of SOME (_, false) => true

     val var = (fst o dest_Var) param
       handle TERM _ => bad "Not an abstype certificate";
     val _ = if param = rhs then () else bad "Not an abstype certificate";
     val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy (abs, Logic.unvarifyT_global raw_ty);
     val ty = domain_type ty';
+    val vs' = map dest_TFree (Sign.const_typargs thy (abs, ty'));
     val ty_abs = range_type ty';
-  in (tyco, (vs ~~ sorts, ((abs, ty), (rep, thm)))) end;
+  in (tyco, (vs ~~ sorts, ((abs, (vs', ty)), (rep, thm)))) end;
 
 
 (* code equation certificates *)
 
 fun build_head thy (c, ty) =

         val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
       in Equations (cert_thm, propers) end;
 
 fun cert_of_proj thy c tyco =
   let
-    val (vs, ((abs, ty), (rep, cert))) = get_abstype_spec thy tyco;
+    val (vs, ((abs, (_, ty)), (rep, cert))) = get_abstype_spec thy tyco;
     val _ = if c = rep then () else
       error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
   in Projection (mk_proj tyco vs ty abs rep, tyco) end;
 
 fun cert_of_abs thy tyco c raw_abs_thm =

       then pretty_typ typ
       else (Pretty.block o Pretty.breaks) (
         pretty_typ typ
         :: Pretty.str "="
         :: (if abstract then [Pretty.str "(abstract)"] else [])
-        @ separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c)
-             | (c, tys) =>
+        @ separate (Pretty.str "|") (map (fn (c, (_, [])) => Pretty.str (string_of_const thy c)
+             | (c, (_, tys)) =>
                  (Pretty.block o Pretty.breaks)
                     (Pretty.str (string_of_const thy c)
                       :: Pretty.str "of"
                       :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
       );

 
 structure Datatype_Interpretation =
   Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
 
 fun datatype_interpretation f = Datatype_Interpretation.interpretation
-  (fn (tyco, _) => fn thy => f (tyco, fst (get_type_spec thy tyco)) thy);
+  (fn (tyco, _) => fn thy => f (tyco, fst (get_type thy tyco)) thy);
 
 fun add_datatype proto_constrs thy =
   let
     val constrs = map (unoverload_const_typ thy) proto_constrs;
     val (tyco, (vs, cos)) = constrset_of_consts thy constrs;

 fun abstype_interpretation f = Abstype_Interpretation.interpretation
   (fn (tyco, _) => fn thy => f (tyco, get_abstype_spec thy tyco) thy);
 
 fun add_abstype proto_thm thy =
   let
-    val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert)))) =
+    val (tyco, (vs, (abs_ty as (abs, (_, ty)), (rep, cert)))) =
       error_thm (check_abstype_cert thy) proto_thm;
   in
     thy
     |> del_eqns abs
     |> register_type (tyco, (vs, Abstractor (abs_ty, (rep, cert))))