changeset 67703 | 8c4806fe827f |
parent 63859 | dca6fabd8060 |
child 69593 | 3dda49e08b9d |
--- a/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Feb 23 14:12:48 2018 +0100 +++ b/src/HOL/Tools/Transfer/transfer_bnf.ML Fri Feb 23 14:32:59 2018 +0100 @@ -38,9 +38,6 @@ fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst -fun is_Type (Type _) = true - | is_Type _ = false - fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I fun bnf_of_fp_sugar (fp_sugar:fp_sugar) = nth (#bnfs (#fp_res fp_sugar)) (#fp_res_index fp_sugar)