156 | NONE => lthy |> |
156 | NONE => lthy |> |
157 Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); |
157 Generic_Target.theory_foundation (((b, U), mx), (b_def, rhs)) (type_params, term_params); |
158 |
158 |
159 fun pretty lthy = |
159 fun pretty lthy = |
160 let |
160 let |
161 val thy = ProofContext.theory_of lthy; |
|
162 val overloading = get_overloading lthy; |
161 val overloading = get_overloading lthy; |
163 fun pr_operation ((c, ty), (v, _)) = |
162 fun pr_operation ((c, ty), (v, _)) = |
164 (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==", |
163 Pretty.block (Pretty.breaks |
165 Pretty.str (Sign.extern_const thy c), Pretty.str "::", Syntax.pretty_typ lthy ty]; |
164 [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c), |
|
165 Pretty.str "::", Syntax.pretty_typ lthy ty]); |
166 in Pretty.str "overloading" :: map pr_operation overloading end; |
166 in Pretty.str "overloading" :: map pr_operation overloading end; |
167 |
167 |
168 fun conclude lthy = |
168 fun conclude lthy = |
169 let |
169 let |
170 val overloading = get_overloading lthy; |
170 val overloading = get_overloading lthy; |