src/Pure/sign.ML
changeset 42381 309ec68442c6
parent 42376 c3abf2c3f541
child 42383 0ae4ad40d7b5
     1.1 --- a/src/Pure/sign.ML	Sun Apr 17 21:17:45 2011 +0200
     1.2 +++ b/src/Pure/sign.ML	Sun Apr 17 21:42:47 2011 +0200
     1.3 @@ -401,7 +401,7 @@
     1.4        let
     1.5          val c = full_name thy b;
     1.6          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
     1.7 -          cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
     1.8 +          cat_error msg ("in declaration of constant " ^ Binding.print b);
     1.9          val T' = Logic.varifyT_global T;
    1.10        in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end;
    1.11      val args = map prep raw_args;
    1.12 @@ -432,7 +432,7 @@
    1.13      val ctxt = Syntax.init_pretty_global thy;
    1.14      val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy;
    1.15      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    1.16 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
    1.17 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
    1.18      val (res, consts') = consts_of thy
    1.19        |> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
    1.20    in (res, thy |> map_consts (K consts')) end;