# HG changeset patch
# User wenzelm
# Date 1254258897 -7200
# Node ID 2885e2a09f7284283604002128f9b1935bfb55fe
# Parent  87491cac8b83a73ddb48161c821f6b0e2bd018d1
removed dead/duplicate code;

diff -r 87491cac8b83 -r 2885e2a09f72 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Tue Sep 29 22:53:07 2009 +0200
+++ b/src/HOL/Tools/record.ML	Tue Sep 29 23:14:57 2009 +0200
@@ -1732,31 +1732,8 @@
 
     (*before doing anything else, create the tree of new types
       that will back the record extension*)
-    (* FIXME cf. Balanced_Tree.make *)
-    fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
-      | mktreeT [T] = T
-      | mktreeT xs =
-          let
-            val len = length xs;
-            val half = len div 2;
-            val left = List.take (xs, half);
-            val right = List.drop (xs, half);
-          in
-            HOLogic.mk_prodT (mktreeT left, mktreeT right)
-          end;
-
-    (* FIXME cf. Balanced_Tree.make *)
-    fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
-      | mktreeV [T] = T
-      | mktreeV xs =
-          let
-            val len = length xs;
-            val half = len div 2;
-            val left = List.take (xs, half);
-            val right = List.drop (xs, half);
-          in
-            IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
-          end;
+
+    val mktreeV = Balanced_Tree.make IsTupleSupport.mk_cons_tuple;
 
     fun mk_istuple (left, right) (thy, i) =
       let