pretty_abbrev: read abbreviation more directly;
authorwenzelm
Mon Apr 18 23:41:15 2011 +0200 (2011-04-18)
changeset 4239995b17b4901b5
parent 42398 919e17c0358e
child 42400 26c8c9cabb24
pretty_abbrev: read abbreviation more directly;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Apr 18 20:40:31 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Mon Apr 18 23:41:15 2011 +0200
     1.3 @@ -498,7 +498,7 @@
     1.4  
     1.5  fun pretty_abbrev ctxt s =
     1.6    let
     1.7 -    val t = Syntax.parse_term ctxt s |> singleton (Proof_Context.standard_infer_types ctxt);
     1.8 +    val t = Syntax.read_term (Proof_Context.set_mode Proof_Context.mode_abbrev ctxt) s;
     1.9      fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
    1.10      val (head, args) = Term.strip_comb t;
    1.11      val (c, T) = Term.dest_Const head handle TERM _ => err ();