added Binding.print convenience, which includes quote already;
authorwenzelm
Sun Apr 17 21:42:47 2011 +0200 (2011-04-17 ago)
changeset 42381309ec68442c6
parent 42380 9371ea9f91fb
child 42382 dcd983ee2c29
child 42390 be7af468f7b3
added Binding.print convenience, which includes quote already;
src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
src/HOL/HOLCF/Tools/cont_consts.ML
src/HOL/HOLCF/Tools/cpodef.ML
src/HOL/HOLCF/Tools/domaindef.ML
src/HOL/Tools/Datatype/datatype.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/record.ML
src/HOL/Tools/typedef.ML
src/Pure/General/binding.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/generic_target.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/typedecl.ML
src/Pure/consts.ML
src/Pure/global_theory.ML
src/Pure/pure_setup.ML
src/Pure/sign.ML
src/Pure/theory.ML
src/Pure/type.ML
     1.1 --- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Apr 17 21:17:45 2011 +0200
     1.2 +++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML	Sun Apr 17 21:42:47 2011 +0200
     1.3 @@ -462,7 +462,7 @@
     1.4            [] =>
     1.5              if eq_set (op =) (tyvars, tvs) then (full_tname, tvs)
     1.6              else error ("Mutually recursive domains must have same type parameters")
     1.7 -        | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^
     1.8 +        | dups => error ("Duplicate parameter(s) for domain " ^ Binding.print tname ^
     1.9              " : " ^ commas dups))
    1.10        end) doms
    1.11      val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms
     2.1 --- a/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Apr 17 21:17:45 2011 +0200
     2.2 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML	Sun Apr 17 21:42:47 2011 +0200
     2.3 @@ -65,7 +65,7 @@
     2.4    | is_contconst (c, T, mx) =
     2.5        let
     2.6          val n = Mixfix.mixfix_args mx handle ERROR msg =>
     2.7 -          cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c))
     2.8 +          cat_error msg ("in mixfix annotation for " ^ Binding.print c)
     2.9        in cfun_arity T >= n end
    2.10  
    2.11  
     3.1 --- a/src/HOL/HOLCF/Tools/cpodef.ML	Sun Apr 17 21:17:45 2011 +0200
     3.2 +++ b/src/HOL/HOLCF/Tools/cpodef.ML	Sun Apr 17 21:42:47 2011 +0200
     3.3 @@ -237,7 +237,7 @@
     3.4      (goal_nonempty, goal_admissible, cpodef_result)
     3.5    end
     3.6    handle ERROR msg =>
     3.7 -    cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name))
     3.8 +    cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print name)
     3.9  
    3.10  fun prepare_pcpodef
    3.11        (prep_term: Proof.context -> 'a -> term)
    3.12 @@ -274,7 +274,7 @@
    3.13      (goal_bottom_mem, goal_admissible, pcpodef_result)
    3.14    end
    3.15    handle ERROR msg =>
    3.16 -    cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name))
    3.17 +    cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print name)
    3.18  
    3.19  
    3.20  (* tactic interface *)
     4.1 --- a/src/HOL/HOLCF/Tools/domaindef.ML	Sun Apr 17 21:17:45 2011 +0200
     4.2 +++ b/src/HOL/HOLCF/Tools/domaindef.ML	Sun Apr 17 21:42:47 2011 +0200
     4.3 @@ -197,7 +197,7 @@
     4.4      ((info, cpo_info, pcpo_info, rep_info), thy)
     4.5    end
     4.6    handle ERROR msg =>
     4.7 -    cat_error msg ("The error(s) above occurred in domaindef " ^ quote (Binding.str_of name))
     4.8 +    cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print name)
     4.9  
    4.10  fun add_domaindef def opt_name typ defl opt_morphs thy =
    4.11    let
     5.1 --- a/src/HOL/Tools/Datatype/datatype.ML	Sun Apr 17 21:17:45 2011 +0200
     5.2 +++ b/src/HOL/Tools/Datatype/datatype.ML	Sun Apr 17 21:42:47 2011 +0200
     5.3 @@ -660,7 +660,7 @@
     5.4            [] =>
     5.5              if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
     5.6              else error ("Mutually recursive datatypes must have same type parameters")
     5.7 -        | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
     5.8 +        | dups => error ("Duplicate parameter(s) for datatype " ^ Binding.print tname ^
     5.9              " : " ^ commas dups))
    5.10        end) dts);
    5.11      val dt_names = map fst new_dts;
    5.12 @@ -684,8 +684,8 @@
    5.13              (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')],
    5.14                constr_syntax' @ [(cname, mx')], sorts'')
    5.15            end handle ERROR msg => cat_error msg
    5.16 -           ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
    5.17 -            " of datatype " ^ quote (Binding.str_of tname));
    5.18 +           ("The error above occurred in constructor " ^ Binding.print cname ^
    5.19 +            " of datatype " ^ Binding.print tname);
    5.20  
    5.21          val (constrs', constr_syntax', sorts') =
    5.22            fold prep_constr constrs ([], [], sorts)
    5.23 @@ -694,8 +694,8 @@
    5.24            [] =>
    5.25              (dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
    5.26                constr_syntax @ [constr_syntax'], sorts', i + 1)
    5.27 -        | dups => error ("Duplicate constructors " ^ commas dups ^
    5.28 -             " in datatype " ^ quote (Binding.str_of tname))
    5.29 +        | dups =>
    5.30 +            error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname)
    5.31        end;
    5.32  
    5.33      val (dts', constr_syntax, sorts', i) =
     6.1 --- a/src/HOL/Tools/inductive.ML	Sun Apr 17 21:17:45 2011 +0200
     6.2 +++ b/src/HOL/Tools/inductive.ML	Sun Apr 17 21:42:47 2011 +0200
     6.3 @@ -269,12 +269,12 @@
     6.4  local
     6.5  
     6.6  fun err_in_rule ctxt name t msg =
     6.7 -  error (cat_lines ["Ill-formed introduction rule " ^ quote name,
     6.8 +  error (cat_lines ["Ill-formed introduction rule " ^ Binding.print name,
     6.9      Syntax.string_of_term ctxt t, msg]);
    6.10  
    6.11  fun err_in_prem ctxt name t p msg =
    6.12    error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p,
    6.13 -    "in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]);
    6.14 +    "in introduction rule " ^ Binding.print name, Syntax.string_of_term ctxt t, msg]);
    6.15  
    6.16  val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
    6.17  
    6.18 @@ -288,7 +288,6 @@
    6.19  
    6.20  fun check_rule ctxt cs params ((binding, att), rule) =
    6.21    let
    6.22 -    val err_name = Binding.str_of binding;
    6.23      val params' = Term.variant_frees rule (Logic.strip_params rule);
    6.24      val frees = rev (map Free params');
    6.25      val concl = subst_bounds (frees, Logic.strip_assums_concl rule);
    6.26 @@ -306,7 +305,7 @@
    6.27  
    6.28      fun check_prem' prem t =
    6.29        if member (op =) cs (head_of t) then
    6.30 -        check_ind (err_in_prem ctxt err_name rule prem) t
    6.31 +        check_ind (err_in_prem ctxt binding rule prem) t
    6.32        else (case t of
    6.33            Abs (_, _, t) => check_prem' prem t
    6.34          | t $ u => (check_prem' prem t; check_prem' prem u)
    6.35 @@ -314,15 +313,15 @@
    6.36  
    6.37      fun check_prem (prem, aprem) =
    6.38        if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
    6.39 -      else err_in_prem ctxt err_name rule prem "Non-atomic premise";
    6.40 +      else err_in_prem ctxt binding rule prem "Non-atomic premise";
    6.41    in
    6.42      (case concl of
    6.43         Const (@{const_name Trueprop}, _) $ t =>
    6.44           if member (op =) cs (head_of t) then
    6.45 -           (check_ind (err_in_rule ctxt err_name rule') t;
    6.46 +           (check_ind (err_in_rule ctxt binding rule') t;
    6.47              List.app check_prem (prems ~~ aprems))
    6.48 -         else err_in_rule ctxt err_name rule' bad_concl
    6.49 -     | _ => err_in_rule ctxt err_name rule' bad_concl);
    6.50 +         else err_in_rule ctxt binding rule' bad_concl
    6.51 +     | _ => err_in_rule ctxt binding rule' bad_concl);
    6.52      ((binding, att), arule)
    6.53    end;
    6.54  
     7.1 --- a/src/HOL/Tools/record.ML	Sun Apr 17 21:17:45 2011 +0200
     7.2 +++ b/src/HOL/Tools/record.ML	Sun Apr 17 21:42:47 2011 +0200
     7.3 @@ -2398,7 +2398,7 @@
     7.4  
     7.5  fun prep_field prep (x, T, mx) = (x, prep T, mx)
     7.6    handle ERROR msg =>
     7.7 -    cat_error msg ("The error(s) above occurred in record field " ^ quote (Binding.str_of x));
     7.8 +    cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x);
     7.9  
    7.10  fun read_field raw_field ctxt =
    7.11    let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
    7.12 @@ -2411,7 +2411,7 @@
    7.13      val _ = Theory.requires thy "Record" "record definitions";
    7.14      val _ =
    7.15        if quiet_mode then ()
    7.16 -      else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
    7.17 +      else writeln ("Defining record " ^ Binding.print binding ^ " ...");
    7.18  
    7.19      val ctxt = Proof_Context.init_global thy;
    7.20      fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
    7.21 @@ -2447,7 +2447,7 @@
    7.22      val err_dup_fields =
    7.23        (case duplicates Binding.eq_name (map #1 bfields) of
    7.24          [] => []
    7.25 -      | dups => ["Duplicate field(s) " ^ commas_quote (map Binding.str_of dups)]);
    7.26 +      | dups => ["Duplicate field(s) " ^ commas (map Binding.print dups)]);
    7.27  
    7.28      val err_bad_fields =
    7.29        if forall (not_equal moreN o Binding.name_of o #1) bfields then []
    7.30 @@ -2459,7 +2459,7 @@
    7.31    in
    7.32      thy |> definition (params, binding) parent parents bfields
    7.33    end
    7.34 -  handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
    7.35 +  handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
    7.36  
    7.37  fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
    7.38    let
     8.1 --- a/src/HOL/Tools/typedef.ML	Sun Apr 17 21:17:45 2011 +0200
     8.2 +++ b/src/HOL/Tools/typedef.ML	Sun Apr 17 21:42:47 2011 +0200
     8.3 @@ -254,7 +254,7 @@
     8.4  
     8.5    in ((goal, goal_pat, typedef_result), alias_lthy) end
     8.6    handle ERROR msg =>
     8.7 -    cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
     8.8 +    cat_error msg ("The error(s) above occurred in typedef " ^ Binding.print name);
     8.9  
    8.10  
    8.11  (* add_typedef: tactic interface *)
     9.1 --- a/src/Pure/General/binding.ML	Sun Apr 17 21:17:45 2011 +0200
     9.2 +++ b/src/Pure/General/binding.ML	Sun Apr 17 21:42:47 2011 +0200
     9.3 @@ -30,6 +30,7 @@
     9.4    val prefix: bool -> string -> binding -> binding
     9.5    val conceal: binding -> binding
     9.6    val str_of: binding -> string
     9.7 +  val print: binding -> string
     9.8    val bad: binding -> string
     9.9    val check: binding -> unit
    9.10  end;
    9.11 @@ -123,17 +124,18 @@
    9.12      (true, prefix, qualifier, name, pos));
    9.13  
    9.14  
    9.15 -(* str_of *)
    9.16 +(* print *)
    9.17  
    9.18  fun str_of binding =
    9.19    qualified_name_of binding
    9.20    |> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
    9.21  
    9.22 +val print = quote o str_of;
    9.23 +
    9.24  
    9.25  (* check *)
    9.26  
    9.27 -fun bad binding =
    9.28 -  "Bad name binding: " ^ quote (str_of binding) ^ Position.str_of (pos_of binding);
    9.29 +fun bad binding = "Bad name binding: " ^ print binding ^ Position.str_of (pos_of binding);
    9.30  
    9.31  fun check binding =
    9.32    if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
    10.1 --- a/src/Pure/Isar/expression.ML	Sun Apr 17 21:17:45 2011 +0200
    10.2 +++ b/src/Pure/Isar/expression.ML	Sun Apr 17 21:42:47 2011 +0200
    10.3 @@ -746,7 +746,7 @@
    10.4      val _ =
    10.5        if null extraTs then ()
    10.6        else warning ("Additional type variable(s) in locale specification " ^
    10.7 -        quote (Binding.str_of binding) ^ ": " ^
    10.8 +          Binding.print binding ^ ": " ^
    10.9            commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
   10.10  
   10.11      val predicate_binding =
    11.1 --- a/src/Pure/Isar/generic_target.ML	Sun Apr 17 21:17:45 2011 +0200
    11.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Apr 17 21:42:47 2011 +0200
    11.3 @@ -39,7 +39,7 @@
    11.4    if null extra_tfrees then mx
    11.5    else
    11.6      (Context_Position.if_visible ctxt warning
    11.7 -      ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
    11.8 +      ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
    11.9          commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
   11.10          (if mx = NoSyn then ""
   11.11           else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
    12.1 --- a/src/Pure/Isar/proof_context.ML	Sun Apr 17 21:17:45 2011 +0200
    12.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Apr 17 21:42:47 2011 +0200
    12.3 @@ -952,7 +952,7 @@
    12.4      let
    12.5        val x = Variable.name b;
    12.6        val _ = Lexicon.is_identifier (no_skolem internal x) orelse
    12.7 -        error ("Illegal variable name: " ^ quote (Binding.str_of b));
    12.8 +        error ("Illegal variable name: " ^ Binding.print b);
    12.9  
   12.10        fun cond_tvars T =
   12.11          if internal then T
   12.12 @@ -1031,7 +1031,7 @@
   12.13  fun add_abbrev mode (b, raw_t) ctxt =
   12.14    let
   12.15      val t0 = cert_term (ctxt |> set_mode mode_abbrev) raw_t
   12.16 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
   12.17 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
   12.18      val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
   12.19      val ((lhs, rhs), consts') = consts_of ctxt
   12.20        |> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t);
    13.1 --- a/src/Pure/Isar/typedecl.ML	Sun Apr 17 21:17:45 2011 +0200
    13.2 +++ b/src/Pure/Isar/typedecl.ML	Sun Apr 17 21:42:47 2011 +0200
    13.3 @@ -49,7 +49,7 @@
    13.4  
    13.5  fun global_type lthy (b, raw_args) =
    13.6    let
    13.7 -    fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
    13.8 +    fun err msg = error (msg ^ " in type declaration " ^ Binding.print b);
    13.9  
   13.10      val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
   13.11      val args = map (TFree o Proof_Context.check_tfree lthy) raw_args;
   13.12 @@ -89,7 +89,7 @@
   13.13    let
   13.14      val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
   13.15      val rhs = prep_typ b lthy raw_rhs
   13.16 -      handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
   13.17 +      handle ERROR msg => cat_error msg ("in type abbreviation " ^ Binding.print b);
   13.18    in
   13.19      lthy
   13.20      |> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx)
   13.21 @@ -106,7 +106,7 @@
   13.22        else Context_Position.if_visible ctxt warning
   13.23          ("Ignoring sort constraints in type variables(s): " ^
   13.24            commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
   13.25 -          "\nin type abbreviation " ^ quote (Binding.str_of b));
   13.26 +          "\nin type abbreviation " ^ Binding.print b);
   13.27    in rhs end;
   13.28  
   13.29  in
    14.1 --- a/src/Pure/consts.ML	Sun Apr 17 21:17:45 2011 +0200
    14.2 +++ b/src/Pure/consts.ML	Sun Apr 17 21:42:47 2011 +0200
    14.3 @@ -275,7 +275,7 @@
    14.4      val force_expand = mode = Print_Mode.internal;
    14.5  
    14.6      val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
    14.7 -      error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
    14.8 +      error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);
    14.9  
   14.10      val rhs = raw_rhs
   14.11        |> Term.map_types (Type.cert_typ tsig)
    15.1 --- a/src/Pure/global_theory.ML	Sun Apr 17 21:17:45 2011 +0200
    15.2 +++ b/src/Pure/global_theory.ML	Sun Apr 17 21:42:47 2011 +0200
    15.3 @@ -205,7 +205,7 @@
    15.4  
    15.5  fun read ctxt (b, str) =
    15.6    Syntax.read_prop ctxt str handle ERROR msg =>
    15.7 -    cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
    15.8 +    cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b);
    15.9  
   15.10  fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
   15.11    let
    16.1 --- a/src/Pure/pure_setup.ML	Sun Apr 17 21:17:45 2011 +0200
    16.2 +++ b/src/Pure/pure_setup.ML	Sun Apr 17 21:42:47 2011 +0200
    16.3 @@ -22,7 +22,7 @@
    16.4  toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
    16.5  toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
    16.6  toplevel_pp ["Position", "T"] "Pretty.position";
    16.7 -toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
    16.8 +toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
    16.9  toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
   16.10  toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
   16.11  toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
    17.1 --- a/src/Pure/sign.ML	Sun Apr 17 21:17:45 2011 +0200
    17.2 +++ b/src/Pure/sign.ML	Sun Apr 17 21:42:47 2011 +0200
    17.3 @@ -401,7 +401,7 @@
    17.4        let
    17.5          val c = full_name thy b;
    17.6          val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
    17.7 -          cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
    17.8 +          cat_error msg ("in declaration of constant " ^ Binding.print b);
    17.9          val T' = Logic.varifyT_global T;
   17.10        in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end;
   17.11      val args = map prep raw_args;
   17.12 @@ -432,7 +432,7 @@
   17.13      val ctxt = Syntax.init_pretty_global thy;
   17.14      val prep_tm = no_frees ctxt o Term.no_dummy_patterns o cert_term_abbrev thy;
   17.15      val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg | TERM (msg, _) => error msg)
   17.16 -      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote (Binding.str_of b));
   17.17 +      handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
   17.18      val (res, consts') = consts_of thy
   17.19        |> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
   17.20    in (res, thy |> map_consts (K consts')) end;
    18.1 --- a/src/Pure/theory.ML	Sun Apr 17 21:17:45 2011 +0200
    18.2 +++ b/src/Pure/theory.ML	Sun Apr 17 21:42:47 2011 +0200
    18.3 @@ -169,8 +169,7 @@
    18.4        error ("Illegal sort constraints in primitive specification: " ^
    18.5          commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
    18.6    in (b, Sign.no_vars ctxt t) end
    18.7 -  handle ERROR msg =>
    18.8 -    cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
    18.9 +  handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b);
   18.10  
   18.11  fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
   18.12    let
   18.13 @@ -251,7 +250,7 @@
   18.14      val _ = check_overloading ctxt overloaded lhs_const;
   18.15    in defs |> dependencies ctxt unchecked (SOME name) name lhs_const rhs_consts end
   18.16    handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   18.17 -   [Pretty.str ("The error(s) above occurred in definition " ^ quote (Binding.str_of b) ^ ":"),
   18.18 +   [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
   18.19      Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
   18.20  
   18.21  in
    19.1 --- a/src/Pure/type.ML	Sun Apr 17 21:17:45 2011 +0200
    19.2 +++ b/src/Pure/type.ML	Sun Apr 17 21:42:47 2011 +0200
    19.3 @@ -645,14 +645,13 @@
    19.4  in
    19.5  
    19.6  fun add_type ctxt naming (c, n) =
    19.7 -  if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
    19.8 +  if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c)
    19.9    else map_types (new_decl ctxt naming (c, LogicalType n));
   19.10  
   19.11  fun add_abbrev ctxt naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
   19.12    let
   19.13      fun err msg =
   19.14 -      cat_error msg ("The error(s) above occurred in type abbreviation " ^
   19.15 -        quote (Binding.str_of a));
   19.16 +      cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
   19.17      val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
   19.18        handle TYPE (msg, _, _) => err msg;
   19.19      val _ =