abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
authorwenzelm
Sun Nov 11 20:29:07 2007 +0100 (2007-11-11)
changeset 254072859cf34aaf0
parent 25406 1aa7927a6759
child 25408 156f6f7082b8
abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sun Nov 11 20:29:06 2007 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Nov 11 20:29:07 2007 +0100
     1.3 @@ -446,8 +446,9 @@
     1.4      val ([t'], _) = Variable.import_terms true [t] ctxt;
     1.5    in pretty_term ctxt t' end;
     1.6  
     1.7 -fun pretty_abbrev ctxt t =
     1.8 +fun pretty_abbrev ctxt s =
     1.9    let
    1.10 +    val t = Syntax.parse_term ctxt s |> singleton (ProofContext.standard_infer_types ctxt);
    1.11      fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
    1.12      val (head, args) = Term.strip_comb t;
    1.13      val (c, T) = Term.dest_Const head handle TERM _ => err ();
    1.14 @@ -522,7 +523,7 @@
    1.15    ("term_type", args Args.term (output pretty_term_typ)),
    1.16    ("typeof", args Args.term (output pretty_term_typeof)),
    1.17    ("const", args Args.const_proper (output pretty_const)),
    1.18 -  ("abbrev", args Args.term_abbrev (output pretty_abbrev)),
    1.19 +  ("abbrev", args (Scan.lift Args.name) (output pretty_abbrev)),
    1.20    ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
    1.21    ("text", args (Scan.lift Args.name) (output (K pretty_text))),
    1.22    ("goals", output_goals true),