equal
deleted
inserted
replaced
26 |
26 |
27 val dest_binop_list: string -> term -> term list |
27 val dest_binop_list: string -> term -> term list |
28 val regroup_conv: string -> string -> thm list -> int list -> conv |
28 val regroup_conv: string -> string -> thm list -> int list -> conv |
29 val regroup_union_conv: int list -> conv |
29 val regroup_union_conv: int list -> conv |
30 |
30 |
31 val inst_constrs_of : theory -> typ -> term list |
31 val inst_constrs_of: Proof.context -> typ -> term list |
32 end |
32 end |
33 |
33 |
34 structure Function_Lib: FUNCTION_LIB = |
34 structure Function_Lib: FUNCTION_LIB = |
35 struct |
35 struct |
36 |
36 |
131 regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup} |
131 regroup_conv @{const_abbrev Set.empty} @{const_name Lattices.sup} |
132 (map (fn t => t RS eq_reflection) |
132 (map (fn t => t RS eq_reflection) |
133 (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left})) |
133 (@{thms Un_ac} @ @{thms Un_empty_right} @ @{thms Un_empty_left})) |
134 |
134 |
135 |
135 |
136 fun inst_constrs_of thy (T as Type (name, _)) = |
136 fun inst_constrs_of ctxt (Type (name, Ts)) = |
137 map (fn CnCT as (_, CT) => |
137 map (Ctr_Sugar.mk_ctr Ts) (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt name))) |
138 Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const CnCT)) |
138 | inst_constrs_of _ _ = raise Match |
139 (the (Datatype.get_constrs thy name)) |
|
140 | inst_constrs_of thy _ = raise Match |
|
141 |
139 |
142 end |
140 end |