--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Sun Apr 17 21:42:47 2011 +0200
@@ -462,7 +462,7 @@
[] =>
if eq_set (op =) (tyvars, tvs) then (full_tname, tvs)
else error ("Mutually recursive domains must have same type parameters")
- | dups => error ("Duplicate parameter(s) for domain " ^ quote (Binding.str_of tname) ^
+ | dups => error ("Duplicate parameter(s) for domain " ^ Binding.print tname ^
" : " ^ commas dups))
end) doms
val dbinds = map (fn (_, dbind, _, _, _) => dbind) doms
--- a/src/HOL/HOLCF/Tools/cont_consts.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cont_consts.ML Sun Apr 17 21:42:47 2011 +0200
@@ -65,7 +65,7 @@
| is_contconst (c, T, mx) =
let
val n = Mixfix.mixfix_args mx handle ERROR msg =>
- cat_error msg ("in mixfix annotation for " ^ quote (Binding.str_of c))
+ cat_error msg ("in mixfix annotation for " ^ Binding.print c)
in cfun_arity T >= n end
--- a/src/HOL/HOLCF/Tools/cpodef.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Sun Apr 17 21:42:47 2011 +0200
@@ -237,7 +237,7 @@
(goal_nonempty, goal_admissible, cpodef_result)
end
handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in cpodef " ^ quote (Binding.str_of name))
+ cat_error msg ("The error(s) above occurred in cpodef " ^ Binding.print name)
fun prepare_pcpodef
(prep_term: Proof.context -> 'a -> term)
@@ -274,7 +274,7 @@
(goal_bottom_mem, goal_admissible, pcpodef_result)
end
handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in pcpodef " ^ quote (Binding.str_of name))
+ cat_error msg ("The error(s) above occurred in pcpodef " ^ Binding.print name)
(* tactic interface *)
--- a/src/HOL/HOLCF/Tools/domaindef.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Sun Apr 17 21:42:47 2011 +0200
@@ -197,7 +197,7 @@
((info, cpo_info, pcpo_info, rep_info), thy)
end
handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in domaindef " ^ quote (Binding.str_of name))
+ cat_error msg ("The error(s) above occurred in domaindef " ^ Binding.print name)
fun add_domaindef def opt_name typ defl opt_morphs thy =
let
--- a/src/HOL/Tools/Datatype/datatype.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Sun Apr 17 21:42:47 2011 +0200
@@ -660,7 +660,7 @@
[] =>
if eq_set (op =) (tyvars, tvs) then ((full_tname, tvs), (tname, mx))
else error ("Mutually recursive datatypes must have same type parameters")
- | dups => error ("Duplicate parameter(s) for datatype " ^ quote (Binding.str_of tname) ^
+ | dups => error ("Duplicate parameter(s) for datatype " ^ Binding.print tname ^
" : " ^ commas dups))
end) dts);
val dt_names = map fst new_dts;
@@ -684,8 +684,8 @@
(constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs')],
constr_syntax' @ [(cname, mx')], sorts'')
end handle ERROR msg => cat_error msg
- ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^
- " of datatype " ^ quote (Binding.str_of tname));
+ ("The error above occurred in constructor " ^ Binding.print cname ^
+ " of datatype " ^ Binding.print tname);
val (constrs', constr_syntax', sorts') =
fold prep_constr constrs ([], [], sorts)
@@ -694,8 +694,8 @@
[] =>
(dts' @ [(i, (Sign.full_name tmp_thy tname, map Datatype_Aux.DtTFree tvs, constrs'))],
constr_syntax @ [constr_syntax'], sorts', i + 1)
- | dups => error ("Duplicate constructors " ^ commas dups ^
- " in datatype " ^ quote (Binding.str_of tname))
+ | dups =>
+ error ("Duplicate constructors " ^ commas dups ^ " in datatype " ^ Binding.print tname)
end;
val (dts', constr_syntax, sorts', i) =
--- a/src/HOL/Tools/inductive.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/HOL/Tools/inductive.ML Sun Apr 17 21:42:47 2011 +0200
@@ -269,12 +269,12 @@
local
fun err_in_rule ctxt name t msg =
- error (cat_lines ["Ill-formed introduction rule " ^ quote name,
+ error (cat_lines ["Ill-formed introduction rule " ^ Binding.print name,
Syntax.string_of_term ctxt t, msg]);
fun err_in_prem ctxt name t p msg =
error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p,
- "in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]);
+ "in introduction rule " ^ Binding.print name, Syntax.string_of_term ctxt t, msg]);
val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
@@ -288,7 +288,6 @@
fun check_rule ctxt cs params ((binding, att), rule) =
let
- 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);
@@ -306,7 +305,7 @@
fun check_prem' prem t =
if member (op =) cs (head_of t) then
- check_ind (err_in_prem ctxt err_name rule prem) t
+ check_ind (err_in_prem ctxt binding rule prem) t
else (case t of
Abs (_, _, t) => check_prem' prem t
| t $ u => (check_prem' prem t; check_prem' prem u)
@@ -314,15 +313,15 @@
fun check_prem (prem, aprem) =
if can HOLogic.dest_Trueprop aprem then check_prem' prem prem
- else err_in_prem ctxt err_name rule prem "Non-atomic premise";
+ else err_in_prem ctxt binding rule prem "Non-atomic premise";
in
(case concl of
Const (@{const_name Trueprop}, _) $ t =>
if member (op =) cs (head_of t) then
- (check_ind (err_in_rule ctxt err_name rule') t;
+ (check_ind (err_in_rule ctxt binding rule') t;
List.app check_prem (prems ~~ aprems))
- else err_in_rule ctxt err_name rule' bad_concl
- | _ => err_in_rule ctxt err_name rule' bad_concl);
+ else err_in_rule ctxt binding rule' bad_concl
+ | _ => err_in_rule ctxt binding rule' bad_concl);
((binding, att), arule)
end;
--- a/src/HOL/Tools/record.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/HOL/Tools/record.ML Sun Apr 17 21:42:47 2011 +0200
@@ -2398,7 +2398,7 @@
fun prep_field prep (x, T, mx) = (x, prep T, mx)
handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in record field " ^ quote (Binding.str_of x));
+ cat_error msg ("The error(s) above occurred in record field " ^ Binding.print x);
fun read_field raw_field ctxt =
let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field
@@ -2411,7 +2411,7 @@
val _ = Theory.requires thy "Record" "record definitions";
val _ =
if quiet_mode then ()
- else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ...");
+ else writeln ("Defining record " ^ Binding.print binding ^ " ...");
val ctxt = Proof_Context.init_global thy;
fun cert_typ T = Type.no_tvars (Proof_Context.cert_typ ctxt T)
@@ -2447,7 +2447,7 @@
val err_dup_fields =
(case duplicates Binding.eq_name (map #1 bfields) of
[] => []
- | dups => ["Duplicate field(s) " ^ commas_quote (map Binding.str_of dups)]);
+ | dups => ["Duplicate field(s) " ^ commas (map Binding.print dups)]);
val err_bad_fields =
if forall (not_equal moreN o Binding.name_of o #1) bfields then []
@@ -2459,7 +2459,7 @@
in
thy |> definition (params, binding) parent parents bfields
end
- handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding));
+ handle ERROR msg => cat_error msg ("Failed to define record " ^ Binding.print binding);
fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy =
let
--- a/src/HOL/Tools/typedef.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/HOL/Tools/typedef.ML Sun Apr 17 21:42:47 2011 +0200
@@ -254,7 +254,7 @@
in ((goal, goal_pat, typedef_result), alias_lthy) end
handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in typedef " ^ quote (Binding.str_of name));
+ cat_error msg ("The error(s) above occurred in typedef " ^ Binding.print name);
(* add_typedef: tactic interface *)
--- a/src/Pure/General/binding.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/General/binding.ML Sun Apr 17 21:42:47 2011 +0200
@@ -30,6 +30,7 @@
val prefix: bool -> string -> binding -> binding
val conceal: binding -> binding
val str_of: binding -> string
+ val print: binding -> string
val bad: binding -> string
val check: binding -> unit
end;
@@ -123,17 +124,18 @@
(true, prefix, qualifier, name, pos));
-(* str_of *)
+(* print *)
fun str_of binding =
qualified_name_of binding
|> Markup.markup (Position.markup (pos_of binding) (Markup.binding (name_of binding)));
+val print = quote o str_of;
+
(* check *)
-fun bad binding =
- "Bad name binding: " ^ quote (str_of binding) ^ Position.str_of (pos_of binding);
+fun bad binding = "Bad name binding: " ^ print binding ^ Position.str_of (pos_of binding);
fun check binding =
if Symbol.is_ident (Symbol.explode (name_of binding)) then ()
--- a/src/Pure/Isar/expression.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/Isar/expression.ML Sun Apr 17 21:42:47 2011 +0200
@@ -746,7 +746,7 @@
val _ =
if null extraTs then ()
else warning ("Additional type variable(s) in locale specification " ^
- quote (Binding.str_of binding) ^ ": " ^
+ Binding.print binding ^ ": " ^
commas (map (Syntax.string_of_typ ctxt' o TFree) (sort_wrt #1 extraTs)));
val predicate_binding =
--- a/src/Pure/Isar/generic_target.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/Isar/generic_target.ML Sun Apr 17 21:42:47 2011 +0200
@@ -39,7 +39,7 @@
if null extra_tfrees then mx
else
(Context_Position.if_visible ctxt warning
- ("Additional type variable(s) in specification of " ^ Binding.str_of b ^ ": " ^
+ ("Additional type variable(s) in specification of " ^ Binding.print b ^ ": " ^
commas (map (Syntax.string_of_typ ctxt o TFree) (sort_wrt #1 extra_tfrees)) ^
(if mx = NoSyn then ""
else "\nDropping mixfix syntax " ^ Pretty.string_of (Mixfix.pretty_mixfix mx)));
--- a/src/Pure/Isar/proof_context.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/Isar/proof_context.ML Sun Apr 17 21:42:47 2011 +0200
@@ -952,7 +952,7 @@
let
val x = Variable.name b;
val _ = Lexicon.is_identifier (no_skolem internal x) orelse
- error ("Illegal variable name: " ^ quote (Binding.str_of b));
+ error ("Illegal variable name: " ^ Binding.print b);
fun cond_tvars T =
if internal then T
@@ -1031,7 +1031,7 @@
fun add_abbrev mode (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.str_of b));
+ handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
val [t] = Variable.exportT_terms (Variable.declare_term t0 ctxt) ctxt [t0];
val ((lhs, rhs), consts') = consts_of ctxt
|> Consts.abbreviate ctxt (tsig_of ctxt) (naming_of ctxt) mode (b, t);
--- a/src/Pure/Isar/typedecl.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/Isar/typedecl.ML Sun Apr 17 21:42:47 2011 +0200
@@ -49,7 +49,7 @@
fun global_type lthy (b, raw_args) =
let
- fun err msg = error (msg ^ " in type declaration " ^ quote (Binding.str_of b));
+ fun err msg = error (msg ^ " in type declaration " ^ Binding.print b);
val _ = has_duplicates (eq_fst op =) raw_args andalso err "Duplicate parameters";
val args = map (TFree o Proof_Context.check_tfree lthy) raw_args;
@@ -89,7 +89,7 @@
let
val Type (name, _) = global_type lthy (b, map (rpair dummyS) vs);
val rhs = prep_typ b lthy raw_rhs
- handle ERROR msg => cat_error msg ("in type abbreviation " ^ quote (Binding.str_of b));
+ handle ERROR msg => cat_error msg ("in type abbreviation " ^ Binding.print b);
in
lthy
|> basic_decl (fn _ => Sign.add_type_abbrev lthy (b, vs, rhs)) (b, length vs, mx)
@@ -106,7 +106,7 @@
else Context_Position.if_visible ctxt warning
("Ignoring sort constraints in type variables(s): " ^
commas_quote (map (Syntax.string_of_typ ctxt) (rev ignored)) ^
- "\nin type abbreviation " ^ quote (Binding.str_of b));
+ "\nin type abbreviation " ^ Binding.print b);
in rhs end;
in
--- a/src/Pure/consts.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/consts.ML Sun Apr 17 21:42:47 2011 +0200
@@ -275,7 +275,7 @@
val force_expand = mode = Print_Mode.internal;
val _ = Term.exists_subterm Term.is_Var raw_rhs andalso
- error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b));
+ error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);
val rhs = raw_rhs
|> Term.map_types (Type.cert_typ tsig)
--- a/src/Pure/global_theory.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/global_theory.ML Sun Apr 17 21:42:47 2011 +0200
@@ -205,7 +205,7 @@
fun read ctxt (b, str) =
Syntax.read_prop ctxt str handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in definition " ^ quote (Binding.str_of b));
+ cat_error msg ("The error(s) above occurred in definition " ^ Binding.print b);
fun add prep unchecked overloaded = fold_map (fn ((b, raw_prop), atts) => fn thy =>
let
--- a/src/Pure/pure_setup.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/pure_setup.ML Sun Apr 17 21:42:47 2011 +0200
@@ -22,7 +22,7 @@
toplevel_pp ["Task_Queue", "task"] "Pretty.str o Task_Queue.str_of_task";
toplevel_pp ["Task_Queue", "group"] "Pretty.str o Task_Queue.str_of_group";
toplevel_pp ["Position", "T"] "Pretty.position";
-toplevel_pp ["Binding", "binding"] "Pretty.str o quote o Binding.str_of";
+toplevel_pp ["Binding", "binding"] "Pretty.str o Binding.print";
toplevel_pp ["Thm", "thm"] "Proof_Display.pp_thm";
toplevel_pp ["Thm", "cterm"] "Proof_Display.pp_cterm";
toplevel_pp ["Thm", "ctyp"] "Proof_Display.pp_ctyp";
--- a/src/Pure/sign.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/sign.ML Sun Apr 17 21:42:47 2011 +0200
@@ -401,7 +401,7 @@
let
val c = full_name thy b;
val T = (prepT raw_T handle TYPE (msg, _, _) => error msg) handle ERROR msg =>
- cat_error msg ("in declaration of constant " ^ quote (Binding.str_of b));
+ cat_error msg ("in declaration of constant " ^ Binding.print b);
val T' = Logic.varifyT_global T;
in ((b, T'), (Lexicon.mark_const c, T', mx), Const (c, T)) end;
val args = map prep raw_args;
@@ -432,7 +432,7 @@
val ctxt = Syntax.init_pretty_global thy;
val prep_tm = no_frees ctxt 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.str_of b));
+ handle ERROR msg => cat_error msg ("in constant abbreviation " ^ Binding.print b);
val (res, consts') = consts_of thy
|> Consts.abbreviate ctxt (tsig_of thy) (naming_of thy) mode (b, t);
in (res, thy |> map_consts (K consts')) end;
--- a/src/Pure/theory.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/theory.ML Sun Apr 17 21:42:47 2011 +0200
@@ -169,8 +169,7 @@
error ("Illegal sort constraints in primitive specification: " ^
commas (map (Syntax.string_of_typ (Config.put show_sorts true ctxt)) bad_sorts));
in (b, Sign.no_vars ctxt t) end
- handle ERROR msg =>
- cat_error msg ("The error(s) above occurred in axiom " ^ quote (Binding.str_of b));
+ handle ERROR msg => cat_error msg ("The error(s) above occurred in axiom " ^ Binding.print b);
fun add_axiom ctxt raw_axm thy = thy |> map_axioms (fn axioms =>
let
@@ -251,7 +250,7 @@
val _ = check_overloading ctxt overloaded lhs_const;
in defs |> dependencies ctxt unchecked (SOME name) 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.str_of b) ^ ":"),
+ [Pretty.str ("The error(s) above occurred in definition " ^ Binding.print b ^ ":"),
Pretty.fbrk, Pretty.quote (Syntax.pretty_term ctxt tm)]));
in
--- a/src/Pure/type.ML Sun Apr 17 21:17:45 2011 +0200
+++ b/src/Pure/type.ML Sun Apr 17 21:42:47 2011 +0200
@@ -645,14 +645,13 @@
in
fun add_type ctxt naming (c, n) =
- if n < 0 then error ("Bad type constructor declaration " ^ quote (Binding.str_of c))
+ if n < 0 then error ("Bad type constructor declaration " ^ Binding.print c)
else map_types (new_decl ctxt naming (c, LogicalType n));
fun add_abbrev ctxt naming (a, vs, rhs) tsig = tsig |> map_types (fn types =>
let
fun err msg =
- cat_error msg ("The error(s) above occurred in type abbreviation " ^
- quote (Binding.str_of a));
+ cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
handle TYPE (msg, _, _) => err msg;
val _ =