equal
deleted
inserted
replaced
50 end |
50 end |
51 | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = |
51 | filter_pats thy cons pvars ((pat :: pats, thm) :: pts) = |
52 if fst (strip_comb pat) = cons |
52 if fst (strip_comb pat) = cons |
53 then (pat :: pats, thm) :: (filter_pats thy cons pvars pts) |
53 then (pat :: pats, thm) :: (filter_pats thy cons pvars pts) |
54 else filter_pats thy cons pvars pts |
54 else filter_pats thy cons pvars pts |
55 |
|
56 |
|
57 fun inst_constrs_of thy (T as Type (name, _)) = |
|
58 map (fn (Cn,CT) => |
|
59 Envir.subst_term_types (Sign.typ_match thy (body_type CT, T) Vartab.empty) (Const (Cn, CT))) |
|
60 (the (Datatype.get_constrs thy name)) |
|
61 | inst_constrs_of thy _ = raise Match |
|
62 |
55 |
63 |
56 |
64 fun transform_pat _ avars c_assum ([] , thm) = raise Match |
57 fun transform_pat _ avars c_assum ([] , thm) = raise Match |
65 | transform_pat ctxt avars c_assum (pat :: pats, thm) = |
58 | transform_pat ctxt avars c_assum (pat :: pats, thm) = |
66 let |
59 let |