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