385 fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) = |
385 fun add_cert thy vardeps (c, (proto_lhs, proto_cert)) (rhss, eqngr) = |
386 if can (Graph.get_node eqngr) c then (rhss, eqngr) |
386 if can (Graph.get_node eqngr) c then (rhss, eqngr) |
387 else let |
387 else let |
388 val lhs = map_index (fn (k, (v, _)) => |
388 val lhs = map_index (fn (k, (v, _)) => |
389 (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; |
389 (v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs; |
390 val cert = Code.constrain_cert thy (map snd lhs) proto_cert; |
390 val cert = Code.constrain_cert thy (map (Sign.minimize_sort thy o snd) lhs) proto_cert; |
391 val (vs, rhss') = Code.typargs_deps_of_cert thy cert; |
391 val (vs, rhss') = Code.typargs_deps_of_cert thy cert; |
392 val eqngr' = Graph.new_node (c, (vs, cert)) eqngr; |
392 val eqngr' = Graph.new_node (c, (vs, cert)) eqngr; |
393 in (map (pair c) rhss' @ rhss, eqngr') end; |
393 in (map (pair c) rhss' @ rhss, eqngr') end; |
394 |
394 |
395 fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) = |
395 fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) = |