src/HOL/Tools/record.ML

--- 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;