equal
deleted
inserted
replaced
74 |
74 |
75 fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U) |
75 fun dest_cfunT (Type(@{type_name cfun}, [T, U])) = (T, U) |
76 | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); |
76 | dest_cfunT T = raise TYPE ("dest_cfunT", [T], []); |
77 |
77 |
78 fun capply_const (S, T) = |
78 fun capply_const (S, T) = |
79 Const(@{const_name Rep_CFun}, (S ->> T) --> (S --> T)); |
79 Const(@{const_name Rep_cfun}, (S ->> T) --> (S --> T)); |
80 |
80 |
81 fun cabs_const (S, T) = |
81 fun cabs_const (S, T) = |
82 Const(@{const_name Abs_CFun}, (S --> T) --> (S ->> T)); |
82 Const(@{const_name Abs_cfun}, (S --> T) --> (S ->> T)); |
83 |
83 |
84 fun mk_cabs t = |
84 fun mk_cabs t = |
85 let val T = fastype_of t |
85 let val T = fastype_of t |
86 in cabs_const (Term.domain_type T, Term.range_type T) $ t end |
86 in cabs_const (Term.domain_type T, Term.range_type T) $ t end |
87 |
87 |