Binding.str_of;

--- a/src/HOL/Tools/inductive_package.ML	Tue Mar 03 15:09:07 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Mar 03 15:09:08 2009 +0100
@@ -260,7 +260,7 @@
 
 fun check_rule ctxt cs params ((binding, att), rule) =
   let
-    val err_name = Binding.display binding;
+    val err_name = Binding.str_of binding;
     val params' = Term.variant_frees rule (Logic.strip_params rule);
     val frees = rev (map Free params');
     val concl = subst_bounds (frees, Logic.strip_assums_concl rule);

--- a/src/Pure/Isar/proof_context.ML	Tue Mar 03 15:09:07 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Tue Mar 03 15:09:08 2009 +0100
@@ -1091,7 +1091,7 @@
 fun add_abbrev mode tags (b, raw_t) ctxt =
   let
     val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
-      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
+      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
     val ((lhs, rhs), consts') = consts_of ctxt
       |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);

--- a/src/Pure/pure_setup.ML	Tue Mar 03 15:09:07 2009 +0100
+++ b/src/Pure/pure_setup.ML	Tue Mar 03 15:09:08 2009 +0100
@@ -33,7 +33,7 @@
   map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
 install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
 install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
-install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.display));
+install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.str_of));
 install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
 install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
 install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);

--- a/src/Pure/sign.ML	Tue Mar 03 15:09:07 2009 +0100
+++ b/src/Pure/sign.ML	Tue Mar 03 15:09:08 2009 +0100
@@ -512,7 +512,7 @@
         val c = full_name thy b;
         val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
         val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
-          cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
+          cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
         val T' = Logic.varifyT T;
       in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
     val args = map prep raw_args;
@@ -549,7 +549,7 @@
     val pp = Syntax.pp_global thy;
     val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
     val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
-      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
+      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     val (res, consts') = consts_of thy
       |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
   in (res, thy |> map_consts (K consts')) end;

--- a/src/Pure/theory.ML	Tue Mar 03 15:09:07 2009 +0100
+++ b/src/Pure/theory.ML	Tue Mar 03 15:09:08 2009 +0100
@@ -258,7 +258,7 @@
     val _ = check_overloading thy overloaded lhs_const;
   in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
-   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
+   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
     Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));