src/HOL/Tools/Transfer/transfer_bnf.ML
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)