equal
deleted
inserted
replaced
556 |
556 |
557 |
557 |
558 (**** retrieve definition of constant ****) |
558 (**** retrieve definition of constant ****) |
559 |
559 |
560 fun is_instance thy T1 T2 = |
560 fun is_instance thy T1 T2 = |
561 Sign.typ_instance thy (T1, Type.varifyT T2); |
561 Sign.typ_instance thy (T1, Logic.legacy_varifyT T2); |
562 |
562 |
563 fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) => |
563 fun get_assoc_code thy s T = Option.map snd (Library.find_first (fn ((s', T'), _) => |
564 s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); |
564 s = s' andalso is_instance thy T T') (#consts (CodegenData.get thy))); |
565 |
565 |
566 fun get_aux_code xs = map_filter (fn (m, code) => |
566 fun get_aux_code xs = map_filter (fn (m, code) => |