doc-src/Main/Docs/Main_Doc.thy
changeset 37216 3165bc303f66
parent 35805 1c4a8d3b26d2
child 38323 dc2a61b98bab
equal deleted inserted replaced
37215:91dfe7dccfdf 37216:3165bc303f66
     7 fun pretty_term_type_only ctxt (t, T) =
     7 fun pretty_term_type_only ctxt (t, T) =
     8   (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then ()
     8   (if fastype_of t = Sign.certify_typ (ProofContext.theory_of ctxt) T then ()
     9    else error "term_type_only: type mismatch";
     9    else error "term_type_only: type mismatch";
    10    Syntax.pretty_typ ctxt T)
    10    Syntax.pretty_typ ctxt T)
    11 
    11 
    12 val _ = ThyOutput.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
    12 val _ = Thy_Output.antiquotation "term_type_only" (Args.term -- Args.typ_abbrev)
    13   (fn {source, context, ...} => fn arg =>
    13   (fn {source, context, ...} => fn arg =>
    14     ThyOutput.output
    14     Thy_Output.output
    15       (ThyOutput.maybe_pretty_source (pretty_term_type_only context) source [arg]));
    15       (Thy_Output.maybe_pretty_source (pretty_term_type_only context) source [arg]));
    16 *}
    16 *}
    17 (*>*)
    17 (*>*)
    18 text{*
    18 text{*
    19 
    19 
    20 \begin{abstract}
    20 \begin{abstract}