equal
deleted
inserted
replaced
108 |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts |
108 |> Thm.instantiate' [SOME (Thm.global_ctyp_of thy ty)] var_insts |
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.declare_default_eqns_global (map (rpair true) eqs) |
114 |> fold (Code.add_eqn (Code.Equation, false)) eqs (*FIXME default code equation!?*) |
|
115 end |
114 end |
116 |
115 |
117 fun ensure_partial_term_of_code (tyco, (raw_vs, cs)) thy = |
116 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} |
117 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 |
118 in if has_inst then add_partial_term_of_code tyco raw_vs cs thy else thy end |