src/HOL/Tools/record.ML
changeset 32767 2885e2a09f72
parent 32765 3032c0308019
child 32770 c6e6a4665ff5
equal deleted inserted replaced
32766:87491cac8b83 32767:2885e2a09f72
  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. Balanced_Tree.make *)
  1735 
  1736     fun mktreeT [] = raise TYPE ("mktreeT: empty list", [], [])
  1736     val mktreeV = Balanced_Tree.make IsTupleSupport.mk_cons_tuple;
  1737       | mktreeT [T] = T
       
  1738       | mktreeT xs =
       
  1739           let
       
  1740             val len = length xs;
       
  1741             val half = len div 2;
       
  1742             val left = List.take (xs, half);
       
  1743             val right = List.drop (xs, half);
       
  1744           in
       
  1745             HOLogic.mk_prodT (mktreeT left, mktreeT right)
       
  1746           end;
       
  1747 
       
  1748     (* FIXME cf. Balanced_Tree.make *)
       
  1749     fun mktreeV [] = raise TYPE ("mktreeV: empty list", [], [])
       
  1750       | mktreeV [T] = T
       
  1751       | mktreeV xs =
       
  1752           let
       
  1753             val len = length xs;
       
  1754             val half = len div 2;
       
  1755             val left = List.take (xs, half);
       
  1756             val right = List.drop (xs, half);
       
  1757           in
       
  1758             IsTupleSupport.mk_cons_tuple (mktreeV left, mktreeV right)
       
  1759           end;
       
  1760 
  1737 
  1761     fun mk_istuple (left, right) (thy, i) =
  1738     fun mk_istuple (left, right) (thy, i) =
  1762       let
  1739       let
  1763         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
  1740         val suff = if i = 0 then ext_typeN else inner_typeN ^ string_of_int i;
  1764         val nm = suffix suff (Long_Name.base_name name);
  1741         val nm = suffix suff (Long_Name.base_name name);