400 fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true |
400 fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true |
401 | is_DtTFree _ = false; |
401 | is_DtTFree _ = false; |
402 |
402 |
403 val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; |
403 val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr; |
404 val protoTs as (dataTs, _) = chop k descr |
404 val protoTs as (dataTs, _) = chop k descr |
405 |> (pairself o map) |
405 |> (apply2 o map) |
406 (fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds)); |
406 (fn (_, (T_name, Ds, _)) => (T_name, map (Old_Datatype_Aux.typ_of_dtyp descr) Ds)); |
407 |
407 |
408 val T_names = map fst dataTs; |
408 val T_names = map fst dataTs; |
409 val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0 |
409 val _ = eq_set (op =) (T_names, T_names0) orelse not_mutually_recursive T_names0 |
410 |
410 |
411 val (Ts, Us) = (pairself o map) Type protoTs; |
411 val (Ts, Us) = apply2 (map Type) protoTs; |
412 |
412 |
413 val names = map Long_Name.base_name T_names; |
413 val names = map Long_Name.base_name T_names; |
414 val (auxnames, _) = Name.make_context names |
414 val (auxnames, _) = Name.make_context names |
415 |> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us; |
415 |> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us; |
416 val prefix = space_implode "_" names; |
416 val prefix = space_implode "_" names; |