equal
deleted
inserted
replaced
31 fun mk_Domainp P = |
31 fun mk_Domainp P = |
32 let |
32 let |
33 val PT = fastype_of P |
33 val PT = fastype_of P |
34 val argT = hd (binder_types PT) |
34 val argT = hd (binder_types PT) |
35 in |
35 in |
36 Const (@{const_name Domainp}, PT --> argT --> HOLogic.boolT) $ P |
36 Const (\<^const_name>\<open>Domainp\<close>, PT --> argT --> HOLogic.boolT) $ P |
37 end |
37 end |
38 |
38 |
39 fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst |
39 fun type_name_of_bnf bnf = T_of_bnf bnf |> dest_Type |> fst |
40 |
40 |
41 fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I |
41 fun bnf_only_type_ctr f bnf = if is_Type (T_of_bnf bnf) then f bnf else I |