src/HOL/Tools/inductive_codegen.ML
changeset 33064 ba7ff3f9527a
parent 33063 4d462963a7db
child 33244 db230399f890
equal deleted inserted replaced
33059:d1c9bf0f8ae8 33064:ba7ff3f9527a
   623 (* convert n-tuple to nested pairs *)
   623 (* convert n-tuple to nested pairs *)
   624 
   624 
   625 fun conv_ntuple fs ts p =
   625 fun conv_ntuple fs ts p =
   626   let
   626   let
   627     val k = length fs;
   627     val k = length fs;
   628     val xs = map (fn i => str ("x" ^ string_of_int i)) (0 upto k);
   628     val xs = map_range (fn i => str ("x" ^ string_of_int i)) (k + 1);
   629     val xs' = map (fn Bound i => nth xs (k - i)) ts;
   629     val xs' = map (fn Bound i => nth xs (k - i)) ts;
   630     fun conv xs js =
   630     fun conv xs js =
   631       if js mem fs then
   631       if js mem fs then
   632         let
   632         let
   633           val (p, xs') = conv xs (1::js);
   633           val (p, xs') = conv xs (1::js);