equal
deleted
inserted
replaced
67 fun_names: string list, |
67 fun_names: string list, |
68 funs: term list, |
68 funs: term list, |
69 fun_defs: thm list, |
69 fun_defs: thm list, |
70 fpTs: typ list}; |
70 fpTs: typ list}; |
71 |
71 |
72 fun morph_fp_rec_sugar phi {transfers, fun_names, funs, fun_defs, fpTs} = |
72 fun morph_fp_rec_sugar phi ({transfers, fun_names, funs, fun_defs, fpTs} : fp_rec_sugar) = |
73 {transfers = transfers, |
73 {transfers = transfers, |
74 fun_names = fun_names, |
74 fun_names = fun_names, |
75 funs = map (Morphism.term phi) funs, |
75 funs = map (Morphism.term phi) funs, |
76 fun_defs = map (Morphism.thm phi) fun_defs, |
76 fun_defs = map (Morphism.thm phi) fun_defs, |
77 fpTs = map (Morphism.typ phi) fpTs}; |
77 fpTs = map (Morphism.typ phi) fpTs}; |