dropped make_/dest_ naming convention

--- a/src/HOL/Record.thy	Tue Aug 17 15:17:44 2010 +0200
+++ b/src/HOL/Record.thy	Tue Aug 17 15:19:37 2010 +0200
@@ -10,7 +10,7 @@
 
 theory Record
 imports Plain Quickcheck
-uses ("Tools/quickcheck_record.ML") ("Tools/typecopy.ML") ("Tools/record.ML")
+uses ("Tools/quickcheck_record.ML") ("Tools/record.ML")
 begin
 
 subsection {* Introduction *}
@@ -453,7 +453,6 @@
 subsection {* Record package *}
 
 use "Tools/quickcheck_record.ML"
-use "Tools/typecopy.ML"
 use "Tools/record.ML" setup Record.setup
 
 hide_const (open) Tuple_Isomorphism repr abst iso_tuple_fst iso_tuple_snd

--- a/src/HOL/Tools/record.ML	Tue Aug 17 15:17:44 2010 +0200
+++ b/src/HOL/Tools/record.ML	Tue Aug 17 15:19:37 2010 +0200
@@ -151,7 +151,7 @@
     |> pair (tyco, info)
   end
 
-fun typecopy (raw_tyco, raw_vs) raw_ty constr proj thy =
+fun typecopy (raw_tyco, raw_vs) raw_ty thy =
   let
     val ty = Sign.certify_typ thy raw_ty;
     val ctxt = ProofContext.init_global thy |> Variable.declare_typ ty;
@@ -160,13 +160,12 @@
   in
     thy
     |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn)
-      (HOLogic.mk_UNIV ty) (SOME (proj, constr)) tac
+        (HOLogic.mk_UNIV ty) NONE tac
     |-> (fn (tyco, info) => add_info tyco vs info)
   end;
 
 fun do_typedef b repT alphas thy =
   let
-    val (b_constr, b_proj) = (Binding.prefix_name "make_" b, Binding.prefix_name "dest_" b);
     fun get_info thy tyco { vs, constr, typ = repT, proj_inject, proj_constr, ... } =
       let
         val absT = Type (tyco, map TFree vs);
@@ -175,7 +174,7 @@
       end;
   in
     thy
-    |> typecopy (b, alphas) repT b_constr b_proj
+    |> typecopy (b, alphas) repT
     |-> (fn (tyco, info) => `(fn thy => get_info thy tyco info))
   end;