equal
deleted
inserted
replaced
97 fun union_params (rec_tm, cs) = |
97 fun union_params (rec_tm, cs) = |
98 let val (_,args) = strip_comb rec_tm |
98 let val (_,args) = strip_comb rec_tm |
99 fun is_ind arg = (type_of arg = iT) |
99 fun is_ind arg = (type_of arg = iT) |
100 in case List.filter is_ind (args @ cs) of |
100 in case List.filter is_ind (args @ cs) of |
101 [] => @{const 0} |
101 [] => @{const 0} |
102 | u_args => BalancedTree.make mk_Un u_args |
102 | u_args => Balanced_Tree.make mk_Un u_args |
103 end; |
103 end; |
104 |
104 |
105 |
105 |
106 (*Includes rules for succ and Pair since they are common constructions*) |
106 (*Includes rules for succ and Pair since they are common constructions*) |
107 val elim_rls = |
107 val elim_rls = |