src/HOL/Tools/BNF/bnf_lfp_compat.ML
changeset 56452 0c98c9118407
parent 56002 2028467b4df4
child 56453 00548d372f02
equal deleted inserted replaced
56451:856492b0f755 56452:0c98c9118407
    45     val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars;
    45     val fpTs0 as Type (_, var_As) :: _ = map (body_type o fastype_of o hd o #ctrs) fp_ctr_sugars;
    46     val fpT_names' = map (fst o dest_Type) fpTs0;
    46     val fpT_names' = map (fst o dest_Type) fpTs0;
    47 
    47 
    48     val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
    48     val _ = eq_set (op =) (fpT_names, fpT_names') orelse not_mutually_recursive fpT_names;
    49 
    49 
    50     val (unsorted_As, _) = lthy |> mk_TFrees (length var_As);
    50     val (As_names, _) = lthy |> Variable.variant_fixes (map (fn TVar ((s, _), _) => s) var_As);
    51     val As = map2 (resort_tfree o Type.sort_of_atyp) var_As unsorted_As;
    51     val As = map2 (fn s => fn TVar (_, S) => TFree (s, S)) As_names var_As;
    52     val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';
    52     val fpTs as fpT1 :: _ = map (fn s => Type (s, As)) fpT_names';
    53 
    53 
    54     fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk =
    54     fun nested_Tparentss_indicessss_of parent_Tkks (T as Type (s, _)) kk =
    55       (case try lfp_sugar_of s of
    55       (case try lfp_sugar_of s of
    56         SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ...}) =>
    56         SOME ({T = T0, fp_res = {Ts = mutual_Ts0, ...}, ...}) =>