src/HOL/Tools/record.ML
changeset 32765 3032c0308019
parent 32764 690f9cccf232
child 32767 2885e2a09f72
equal deleted inserted replaced
32764:690f9cccf232 32765:3032c0308019
  1730     val len = length fields;
  1730     val len = length fields;
  1731     val idxms = 0 upto len;
  1731     val idxms = 0 upto len;
  1732 
  1732 
  1733     (*before doing anything else, create the tree of new types
  1733     (*before doing anything else, create the tree of new types
  1734       that will back the record extension*)
  1734       that will back the record extension*)
  1735     (* FIXME cf. BalancedTree.make *)
  1735     (* FIXME cf. Balanced_Tree.make *)
  1736     fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
  1736     fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
  1737       | mktreeT [T] = T
  1737       | mktreeT [T] = T
  1738       | mktreeT xs =
  1738       | mktreeT xs =
  1739           let
  1739           let
  1740             val len = length xs;
  1740             val len = length xs;
  1743             val right = List.drop (xs, half);
  1743             val right = List.drop (xs, half);
  1744           in
  1744           in
  1745             HOLogic.mk_prodT (mktreeT left, mktreeT right)
  1745             HOLogic.mk_prodT (mktreeT left, mktreeT right)
  1746           end;
  1746           end;
  1747 
  1747 
  1748     (* FIXME cf. BalancedTree.make *)
  1748     (* FIXME cf. Balanced_Tree.make *)
  1749     fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
  1749     fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
  1750       | mktreeV [T] = T
  1750       | mktreeV [T] = T
  1751       | mktreeV xs =
  1751       | mktreeV xs =
  1752           let
  1752           let
  1753             val len = length xs;
  1753             val len = length xs;