tuned Const.the_abbreviation;
authorwenzelm
Tue Oct 16 17:06:20 2007 +0200 (2007-10-16)
changeset 25054b15a9a5dc9fe
parent 25053 2b86fac03ec5
child 25055 3bb2ad8b1b37
tuned Const.the_abbreviation;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Tue Oct 16 17:06:19 2007 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Oct 16 17:06:20 2007 +0200
     1.3 @@ -448,7 +448,7 @@
     1.4      fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
     1.5      val (head, args) = Term.strip_comb t;
     1.6      val (c, T) = Term.dest_Const head handle TERM _ => err ();
     1.7 -    val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
     1.8 +    val (U, u) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
     1.9        handle TYPE _ => err ();
    1.10      val t' = Term.betapplys (Envir.expand_atom T (U, u), args);
    1.11    in pretty_term_abbrev ctxt (Logic.mk_equals (t, t')) end;