equal
deleted
inserted
replaced
453 fun pretty_thm_style ctxt (style, th) = |
453 fun pretty_thm_style ctxt (style, th) = |
454 pretty_term ctxt (style (Thm.full_prop_of th)); |
454 pretty_term ctxt (style (Thm.full_prop_of th)); |
455 |
455 |
456 fun pretty_term_typ ctxt (style, t) = |
456 fun pretty_term_typ ctxt (style, t) = |
457 let val t' = style t |
457 let val t' = style t |
458 in pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t') t') end; |
458 in pretty_term ctxt (Type_Infer.constrain (Term.fastype_of t') t') end; |
459 |
459 |
460 fun pretty_term_typeof ctxt (style, t) = |
460 fun pretty_term_typeof ctxt (style, t) = |
461 Syntax.pretty_typ ctxt (Term.fastype_of (style t)); |
461 Syntax.pretty_typ ctxt (Term.fastype_of (style t)); |
462 |
462 |
463 fun pretty_const ctxt c = |
463 fun pretty_const ctxt c = |