Binding.str_of;
authorwenzelm
Tue Mar 03 15:09:08 2009 +0100 (2009-03-03 ago)
changeset 30218cdd82ba2b4fd
parent 30217 894eb2034f02
child 30219 9224f88c1651
Binding.str_of;
src/HOL/Tools/inductive_package.ML
src/Pure/Isar/proof_context.ML
src/Pure/pure_setup.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Tue Mar 03 15:09:07 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Tue Mar 03 15:09:08 2009 +0100
     1.3 @@ -260,7 +260,7 @@
     1.4  
     1.5  fun check_rule ctxt cs params ((binding, att), rule) =
     1.6    let
     1.7 -    val err_name = Binding.display binding;
     1.8 +    val err_name = Binding.str_of binding;
     1.9      val params' = Term.variant_frees rule (Logic.strip_params rule);
    1.10      val frees = rev (map Free params');
    1.11      val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
     2.1 --- a/src/Pure/Isar/proof_context.ML	Tue Mar 03 15:09:07 2009 +0100
     2.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Mar 03 15:09:08 2009 +0100
     2.3 @@ -1091,7 +1091,7 @@
     2.4  fun add_abbrev mode tags (b, raw_t) ctxt =
     2.5    let
     2.6      val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
     2.7 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
     2.8 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
     2.9      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
    2.10      val ((lhs, rhs), consts') = consts_of ctxt
    2.11        |> Consts.abbreviate (Syntax.pp ctxt) (tsig_of ctxt) (naming_of ctxt) mode tags (b, t);
     3.1 --- a/src/Pure/pure_setup.ML	Tue Mar 03 15:09:07 2009 +0100
     3.2 +++ b/src/Pure/pure_setup.ML	Tue Mar 03 15:09:08 2009 +0100
     3.3 @@ -33,7 +33,7 @@
     3.4    map (fn (x, y) => Pretty.str (x ^ "=" ^ y)) o Position.properties_of));
     3.5  install_pp (make_pp ["Thm", "thm"] ProofDisplay.pprint_thm);
     3.6  install_pp (make_pp ["Thm", "cterm"] ProofDisplay.pprint_cterm);
     3.7 -install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.display));
     3.8 +install_pp (make_pp ["Binding", "binding"] (Pretty.pprint o Pretty.str o Binding.str_of));
     3.9  install_pp (make_pp ["Thm", "ctyp"] ProofDisplay.pprint_ctyp);
    3.10  install_pp (make_pp ["Context", "theory"] Context.pprint_thy);
    3.11  install_pp (make_pp ["Context", "theory_ref"] Context.pprint_thy_ref);
     4.1 --- a/src/Pure/sign.ML	Tue Mar 03 15:09:07 2009 +0100
     4.2 +++ b/src/Pure/sign.ML	Tue Mar 03 15:09:08 2009 +0100
     4.3 @@ -512,7 +512,7 @@
     4.4          val c = full_name thy b;
     4.5          val c_syn = if authentic then Syntax.constN ^ c else Binding.base_name b;
     4.6          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
     4.7 -          cat_error msg ("in declaration of constant " ^ quote (Binding.display b));
     4.8 +          cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
     4.9          val T' = Logic.varifyT T;
    4.10        in ((b, T'), (c_syn, T', mx), Const (c, T)) end;
    4.11      val args = map prep raw_args;
    4.12 @@ -549,7 +549,7 @@
    4.13      val pp = Syntax.pp_global thy;
    4.14      val prep_tm = no_frees pp o Term.no_dummy_patterns o cert_term_abbrev thy;
    4.15      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
    4.16 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.display b));
    4.17 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
    4.18      val (res, consts') = consts_of thy
    4.19        |> Consts.abbreviate pp (tsig_of thy) (naming_of thy) mode tags (b, t);
    4.20    in (res, thy |> map_consts (K consts')) end;
     5.1 --- a/src/Pure/theory.ML	Tue Mar 03 15:09:07 2009 +0100
     5.2 +++ b/src/Pure/theory.ML	Tue Mar 03 15:09:08 2009 +0100
     5.3 @@ -258,7 +258,7 @@
     5.4      val _ = check_overloading thy overloaded lhs_const;
     5.5    in defs |> dependencies thy unchecked true name lhs_const rhs_consts end
     5.6    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
     5.7 -   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.display b) ^ ":"),
     5.8 +   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
     5.9      Pretty.fbrk, Pretty.quote (Syntax.pretty_term_global thy tm)]));
    5.10  
    5.11