src/Pure/Thy/thy_output.ML
changeset 25054 b15a9a5dc9fe
parent 24920 2a45e400fdad
child 25241 001ab1d3f567
     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;