equal
deleted
inserted
replaced
94 |
94 |
95 (*Make a datatype's domain: form the union of its set parameters*) |
95 (*Make a datatype's domain: form the union of its set parameters*) |
96 fun union_params (rec_tm, cs) = |
96 fun union_params (rec_tm, cs) = |
97 let val (_,args) = strip_comb rec_tm |
97 let val (_,args) = strip_comb rec_tm |
98 fun is_ind arg = (type_of arg = iT) |
98 fun is_ind arg = (type_of arg = iT) |
99 in case List.filter is_ind (args @ cs) of |
99 in case filter is_ind (args @ cs) of |
100 [] => @{const 0} |
100 [] => @{const 0} |
101 | u_args => Balanced_Tree.make mk_Un u_args |
101 | u_args => Balanced_Tree.make mk_Un u_args |
102 end; |
102 end; |
103 |
103 |
104 |
104 |
105 (*Includes rules for succ and Pair since they are common constructions*) |
105 (*Includes rules for succ and Pair since they are common constructions*) |