@{const}: improved ProofContext.read_const does the job;
authorwenzelm
Sat Nov 10 14:31:23 2007 +0100 (2007-11-10)
changeset 25373ccbf65080fdf
parent 25372 a718f1ccaf1a
child 25374 7657a081fcb4
@{const}: improved ProofContext.read_const does the job;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Nov 10 14:31:22 2007 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Nov 10 14:31:23 2007 +0100
     1.3 @@ -439,10 +439,12 @@
     1.4  
     1.5  fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
     1.6  
     1.7 -fun pretty_term_const ctxt t =
     1.8 -  if Term.is_Const (singleton (Syntax.uncheck_terms ctxt) t)
     1.9 -    then pretty_term ctxt t
    1.10 -    else error ("Constant expected: " ^ Syntax.string_of_term ctxt t);
    1.11 +fun pretty_const ctxt c =
    1.12 +  let
    1.13 +    val t = Const (c, Consts.type_scheme (ProofContext.consts_of ctxt) c)
    1.14 +      handle TYPE (msg, _, _) => error msg;
    1.15 +    val ([t'], _) = Variable.import_terms true [t] ctxt;
    1.16 +  in pretty_term ctxt t' end;
    1.17  
    1.18  fun pretty_abbrev ctxt t =
    1.19    let
    1.20 @@ -519,7 +521,7 @@
    1.21    ("term_style", args (Scan.lift Args.liberal_name -- Args.term) (output pretty_term_style)),
    1.22    ("term_type", args Args.term (output pretty_term_typ)),
    1.23    ("typeof", args Args.term (output pretty_term_typeof)),
    1.24 -  ("const", args Args.term (output pretty_term_const)),
    1.25 +  ("const", args Args.const_proper (output pretty_const)),
    1.26    ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
    1.27    ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
    1.28    ("text", args (Scan.lift Args.name) (output (K pretty_text))),