1.1 --- a/src/HOL/Tools/record.ML	Tue Sep 29 22:53:07 2009 +0200
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Sep 29 23:14:57 2009 +0200
     1.3 @@ -1732,31 +1732,8 @@
     1.4  
     1.5      (*before doing anything else, create the tree of new types
     1.6        that will back the record extension*)
     1.7 -    (* FIXME cf. Balanced_Tree.make *)
     1.8 -    fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
     1.9 -      | mktreeT [T] = T
    1.10 -      | mktreeT xs =
    1.11 -          let
    1.12 -            val len = length xs;
    1.13 -            val half = len div 2;
    1.14 -            val left = List.take (xs, half);
    1.15 -            val right = List.drop (xs, half);
    1.16 -          in
    1.17 -            HOLogic.mk_prodT (mktreeT left, mktreeT right)
    1.18 -          end;
    1.19 -
    1.20 -    (* FIXME cf. Balanced_Tree.make *)
    1.21 -    fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
    1.22 -      | mktreeV [T] = T
    1.23 -      | mktreeV xs =
    1.24 -          let
    1.25 -            val len = length xs;
    1.26 -            val half = len div 2;
    1.27 -            val left = List.take (xs, half);
    1.28 -            val right = List.drop (xs, half);
    1.29 -          in
    1.30 -            IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
    1.31 -          end;
    1.32 +
    1.33 +    val mktreeV = Balanced_Tree.make IsTupleSupport.mk_cons_tuple;
    1.34  
    1.35      fun mk_istuple (left, right) (thy, i) =
    1.36        let