126 |
126 |
127 fun define_projections fixes mutual fsum lthy = |
127 fun define_projections fixes mutual fsum lthy = |
128 let |
128 let |
129 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
129 fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy = |
130 let |
130 let |
|
131 val def_binding = |
|
132 if Config.get lthy function_defs then (Binding.name (Thm.def_name fname), []) |
|
133 else Attrib.empty_binding |
131 val ((f, (_, f_defthm)), lthy') = |
134 val ((f, (_, f_defthm)), lthy') = |
132 Local_Theory.define |
135 Local_Theory.define |
133 ((Binding.name fname, mixfix), |
136 ((Binding.name fname, mixfix), |
134 ((Binding.concealed (Binding.name (Thm.def_name fname)), []), |
137 (def_binding, Term.subst_bound (fsum, f_def))) lthy |
135 Term.subst_bound (fsum, f_def))) lthy |
|
136 in |
138 in |
137 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
139 (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def, |
138 f=SOME f, f_defthm=SOME f_defthm }, |
140 f=SOME f, f_defthm=SOME f_defthm }, |
139 lthy') |
141 lthy') |
140 end |
142 end |