equal
deleted
inserted
replaced
53 val b_names = map Binding.name_of bs; |
53 val b_names = map Binding.name_of bs; |
54 val fp_b_names = map base_name_of_typ fpTs; |
54 val fp_b_names = map base_name_of_typ fpTs; |
55 |
55 |
56 val nn = length fpTs; |
56 val nn = length fpTs; |
57 |
57 |
58 fun target_ctr_sugar_of_fp_sugar fpT {T, index, ctr_sugars, ...} = |
58 fun target_ctr_sugar_of_fp_sugar fpT ({T, index, ctr_sugars, ...} : fp_sugar) = |
59 let |
59 let |
60 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) []; |
60 val rho = Vartab.fold (cons o apsnd snd) (Sign.typ_match thy (T, fpT) Vartab.empty) []; |
61 val phi = Morphism.term_morphism (Term.subst_TVars rho); |
61 val phi = Morphism.term_morphism (Term.subst_TVars rho); |
62 in |
62 in |
63 morph_ctr_sugar phi (nth ctr_sugars index) |
63 morph_ctr_sugar phi (nth ctr_sugars index) |