equal
deleted
inserted
replaced
1163 t1 $ t2 => |
1163 t1 $ t2 => |
1164 if quant_s = "" then |
1164 if quant_s = "" then |
1165 aux "" [] [] t1 $ aux "" [] [] t2 |
1165 aux "" [] [] t1 $ aux "" [] [] t2 |
1166 else |
1166 else |
1167 let |
1167 let |
1168 val typical_card = 4 |
|
1169 fun big_union proj ps = |
1168 fun big_union proj ps = |
1170 fold (fold (insert (op =)) o proj) ps [] |
1169 fold (fold (insert (op =)) o proj) ps [] |
1171 val (ts, connective) = strip_any_connective t |
1170 val (ts, connective) = strip_any_connective t |
1172 val T_costs = |
1171 val T_costs = map typical_card_of_type Ts |
1173 map (bounded_card_of_type 65536 typical_card []) Ts |
|
1174 val t_costs = map size_of_term ts |
1172 val t_costs = map size_of_term ts |
1175 val num_Ts = length Ts |
1173 val num_Ts = length Ts |
1176 val flip = curry (op -) (num_Ts - 1) |
1174 val flip = curry (op -) (num_Ts - 1) |
1177 val t_boundss = map (map flip o loose_bnos) ts |
1175 val t_boundss = map (map flip o loose_bnos) ts |
1178 fun merge costly_boundss [] = costly_boundss |
1176 fun merge costly_boundss [] = costly_boundss |