src/HOL/Tools/record.ML
changeset 32767 2885e2a09f72
parent 32765 3032c0308019
child 32770 c6e6a4665ff5
--- 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