# HG changeset patch
# User wenzelm
# Date 1303069367 -7200
# Node ID 309ec68442c6254c725173c0b12a4fe4f4360910
# Parent  9371ea9f91fb58408925a38b861fe7a07a71495c
added Binding.print convenience, which includes quote already;

diff -r 9371ea9f91fb -r 309ec68442c6 src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML
--- 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
diff -r 9371ea9f91fb -r 309ec68442c6 src/HOL/HOLCF/Tools/cont_consts.ML
--- 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
 
 
diff -r 9371ea9f91fb -r 309ec68442c6 src/HOL/HOLCF/Tools/cpodef.ML
--- 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 *)
diff -r 9371ea9f91fb -r 309ec68442c6 src/HOL/HOLCF/Tools/domaindef.ML
--- 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
diff -r 9371ea9f91fb -r 309ec68442c6 src/HOL/Tools/Datatype/datatype.ML
--- 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) =
diff -r 9371ea9f91fb -r 309ec68442c6 src/HOL/Tools/inductive.ML
--- 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;
 
diff -r 9371ea9f91fb -r 309ec68442c6 src/HOL/Tools/record.ML
--- 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
diff -r 9371ea9f91fb -r 309ec68442c6 src/HOL/Tools/typedef.ML
--- 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 *)
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/General/binding.ML
--- 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 ()
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/Isar/expression.ML
--- 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 =
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/Isar/generic_target.ML
--- 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)));
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/Isar/proof_context.ML
--- 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);
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/Isar/typedecl.ML
--- 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
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/consts.ML
--- 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)
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/global_theory.ML
--- 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
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/pure_setup.ML
--- 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";
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/sign.ML
--- 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;
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/theory.ML
--- 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
diff -r 9371ea9f91fb -r 309ec68442c6 src/Pure/type.ML
--- 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 _ =