tuned

--- a/src/HOL/Tools/quickcheck_generators.ML	Fri Aug 14 21:36:14 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Aug 15 15:29:53 2009 +0200
@@ -321,24 +321,23 @@
 
 fun ensure_random_datatype config raw_tycos thy =
   let
-    val pp = Syntax.pp_global thy;
     val algebra = Sign.classes_of thy;
     val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) =
       Datatype.the_descr thy raw_tycos;
-    val typrep_vs = (map o apsnd)
+    val typerep_vs = (map o apsnd)
       (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs;
     val random_insts = (map (rpair @{sort random}) o flat o maps snd o maps snd)
-      (DatatypeAux.interpret_construction descr typrep_vs
+      (DatatypeAux.interpret_construction descr typerep_vs
         { atyp = single, dtyp = (K o K o K) [] });
     val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd)
-      (DatatypeAux.interpret_construction descr typrep_vs
+      (DatatypeAux.interpret_construction descr typerep_vs
         { atyp = K [], dtyp = K o K });
     val has_inst = exists (fn tyco =>
       can (Sorts.mg_domain algebra tyco) @{sort random}) tycos;
   in if has_inst then thy
-    else case perhaps_constrain thy (random_insts @ term_of_insts) typrep_vs
+    else case perhaps_constrain thy (random_insts @ term_of_insts) typerep_vs
      of SOME constrain => mk_random_datatype config descr
-          (map constrain typrep_vs) tycos prfx (names, auxnames)
+          (map constrain typerep_vs) tycos prfx (names, auxnames)
             ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy
       | NONE => thy
   end;

--- a/src/HOL/Tools/typecopy.ML	Fri Aug 14 21:36:14 2009 +0200
+++ b/src/HOL/Tools/typecopy.ML	Sat Aug 15 15:29:53 2009 +0200
@@ -91,11 +91,10 @@
 
 fun add_default_code tyco thy =
   let
-    val SOME { constr = constr_name, proj = (proj, _), proj_def = proj_eq, vs = raw_vs,
+    val SOME { constr = c, proj = (proj, _), proj_def = proj_eq, vs = vs,
       typ = ty_rep, ... } =  get_info thy tyco;
     val SOME { Rep_inject = proj_inject, ... } = Typedef.get_info thy tyco;
-    val constr = (constr_name, Logic.unvarifyT (Sign.the_const_type thy constr_name));
-    val vs = (map dest_TFree o snd o dest_Type) (Type (tyco, map TFree raw_vs));
+    val constr = (c, Logic.unvarifyT (Sign.the_const_type thy c));
     val ty = Type (tyco, map TFree vs);
     val proj = Const (proj, ty --> ty_rep);
     val (t_x, t_y) = (Free ("x", ty), Free ("y", ty));