1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Wed Jul 11 11:36:06 2007 +0200
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Wed Jul 11 11:38:25 2007 +0200
     1.3 @@ -615,18 +615,57 @@
     1.4    | SOME _ =>
     1.5        (add_edge (name, dep) gr, mk_qual_id module (get_const_id name gr));
     1.6  
     1.7 +(* convert n-tuple to nested pairs *)
     1.8 +
     1.9 +fun conv_ntuple fs ts p =
    1.10 +  let
    1.11 +    val k = length fs;
    1.12 +    val xs = map (fn i => Pretty.str ("x" ^ string_of_int i)) (0 upto k);
    1.13 +    val xs' = map (fn Bound i => nth xs (k - i)) ts;
    1.14 +    fun conv xs js =
    1.15 +      if js mem fs then
    1.16 +        let
    1.17 +          val (p, xs') = conv xs (1::js);
    1.18 +          val (q, xs'') = conv xs' (2::js)
    1.19 +        in (mk_tuple [p, q], xs'') end
    1.20 +      else (hd xs, tl xs)
    1.21 +  in
    1.22 +    if k > 0 then
    1.23 +      Pretty.block
    1.24 +        [Pretty.str "Seq.map (fn", Pretty.brk 1,
    1.25 +         mk_tuple xs', Pretty.str " =>", Pretty.brk 1, fst (conv xs []),
    1.26 +         Pretty.str ")", Pretty.brk 1, parens p]
    1.27 +    else p
    1.28 +  end;
    1.29 +
    1.30  fun inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
    1.31 -    (Const ("Collect", Type (_, [_, Type (_, [U])])), [u]) => (case strip_comb u of
    1.32 -        (Const (s, T), ts) => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
    1.33 -          (SOME (names, thyname, k, intrs), NONE) =>
    1.34 -            let val (gr', call_p) = mk_ind_call thy defs gr dep module true
    1.35 -              s T (ts @ [Term.dummy_pattern U]) names thyname k intrs
    1.36 -            in SOME (gr', (if brack then parens else I) (Pretty.block
    1.37 -              [Pretty.str "Seq.list_of", Pretty.brk 1, Pretty.str "(",
    1.38 -               call_p, Pretty.str ")"]))
    1.39 -            end
    1.40 -        | _ => NONE)
    1.41 -      | _ => NONE)
    1.42 +    (Const ("Collect", _), [u]) =>
    1.43 +      let val (r, Ts, fs) = HOLogic.strip_split u
    1.44 +      in case strip_comb r of
    1.45 +          (Const (s, T), ts) =>
    1.46 +            (case (get_clauses thy s, get_assoc_code thy (s, T)) of
    1.47 +              (SOME (names, thyname, k, intrs), NONE) =>
    1.48 +                let
    1.49 +                  val (ts1, ts2) = chop k ts;
    1.50 +                  val ts2' = map
    1.51 +                    (fn Bound i => Term.dummy_pattern (nth Ts i) | t => t) ts2;
    1.52 +                  val (ots, its) = List.partition is_Bound ts2;
    1.53 +                  val no_loose = forall (fn t => not (loose_bvar (t, 0)))
    1.54 +                in
    1.55 +                  if null (duplicates op = ots) andalso
    1.56 +                    no_loose ts1 andalso no_loose its
    1.57 +                  then
    1.58 +                    let val (gr', call_p) = mk_ind_call thy defs gr dep module true
    1.59 +                      s T (ts1 @ ts2') names thyname k intrs
    1.60 +                    in SOME (gr', (if brack then parens else I) (Pretty.block
    1.61 +                      [Pretty.str "Seq.list_of", Pretty.brk 1, Pretty.str "(",
    1.62 +                       conv_ntuple fs ots call_p, Pretty.str ")"]))
    1.63 +                    end
    1.64 +                  else NONE
    1.65 +                end
    1.66 +            | _ => NONE)
    1.67 +        | _ => NONE
    1.68 +      end
    1.69    | (Const (s, T), ts) => (case Symtab.lookup (#eqns (CodegenData.get thy)) s of
    1.70        NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
    1.71          (SOME (names, thyname, k, intrs), NONE) =>