equal
deleted
inserted
replaced
109 |> Thm.varifyT_global |
109 |> Thm.varifyT_global |
110 val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs |
110 val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs |
111 in |
111 in |
112 thy |
112 thy |
113 |> Code.del_eqns const |
113 |> Code.del_eqns const |
114 |> fold Code.add_eqn eqs |
114 |> fold (Code.add_eqn (Code.Equation, false)) eqs (*FIXME default code equation!?*) |
115 end |
115 end |
116 |
116 |
117 fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = |
117 fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = |
118 let val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of} |
118 let val has_inst = Sorts.has_instance (Sign.classes_of thy) tyco @{sort partial_term_of} |
119 in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end |
119 in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end |