equal
deleted
inserted
replaced
584 structure Extra_Norms = Generic_Data |
584 structure Extra_Norms = Generic_Data |
585 ( |
585 ( |
586 type T = extra_norm U.dict |
586 type T = extra_norm U.dict |
587 val empty = [] |
587 val empty = [] |
588 val extend = I |
588 val extend = I |
589 val merge = U.dict_merge fst |
589 fun merge xx = U.dict_merge fst xx |
590 ) |
590 ) |
591 |
591 |
592 fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm)) |
592 fun add_extra_norm (cs, norm) = Extra_Norms.map (U.dict_update (cs, norm)) |
593 |
593 |
594 fun apply_extra_norms ctxt = |
594 fun apply_extra_norms ctxt = |