src/Pure/Isar/proof_context.ML
changeset 30218 cdd82ba2b4fd
parent 30211 556d1810cdad
child 30223 24d975352879
     1.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 03 15:09:07 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 03 15:09:08 2009 +0100
     1.3 @@ -1091,7 +1091,7 @@
     1.4  fun add_abbrev mode tags (b, raw_t) ctxt =
     1.5    let
     1.6      val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
     1.7 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
     1.8 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     1.9      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
    1.10      val ((lhs, rhs), consts') = consts_of ctxt
    1.11        |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);