equal
deleted
inserted
replaced
105 case try (Graph.get_node eqngr) c |
105 case try (Graph.get_node eqngr) c |
106 of SOME ((lhs, _), eqns) => ((lhs, []), []) |
106 of SOME ((lhs, _), eqns) => ((lhs, []), []) |
107 | NONE => let |
107 | NONE => let |
108 val eqns = Code.these_eqns thy c |
108 val eqns = Code.these_eqns thy c |
109 |> burrow_fst (Code_Unit.norm_args thy) |
109 |> burrow_fst (Code_Unit.norm_args thy) |
110 |> burrow_fst (Code_Unit.norm_varnames thy Code_Name.purify_tvar Code_Name.purify_var); |
110 |> burrow_fst (Code_Unit.norm_varnames thy); |
111 val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns; |
111 val ((lhs, _), rhss) = tyscm_rhss_of thy c eqns; |
112 in ((lhs, rhss), eqns) end; |
112 in ((lhs, rhss), eqns) end; |
113 |
113 |
114 fun obtain_instance thy arities (inst as (class, tyco)) = |
114 fun obtain_instance thy arities (inst as (class, tyco)) = |
115 case AList.lookup (op =) arities inst |
115 case AList.lookup (op =) arities inst |