# HG changeset patch
# User wenzelm
# Date 1378909005 -7200
# Node ID 73d4c76d8eb2dfb3fe547f59f34b9ad922b2f0b9
# Parent  d0c163c6c725a848e420e5b016b5ccc9129cd1cb# Parent  7903fe2c271b9173c232d39b4195c5a447f913f5
merged

diff -r d0c163c6c725 -r 73d4c76d8eb2 src/Doc/IsarRef/Spec.thy
--- a/src/Doc/IsarRef/Spec.thy	Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Doc/IsarRef/Spec.thy	Wed Sep 11 16:16:45 2013 +0200
@@ -251,7 +251,7 @@
   Here is an artificial example of bundling various configuration
   options: *}
 
-bundle trace = [[simp_trace, blast_trace, linarith_trace, metis_trace, smt_trace]]
+bundle trace = [[simp_trace, linarith_trace, metis_trace, smt_trace]]
 
 lemma "x = x"
   including trace by metis
diff -r d0c163c6c725 -r 73d4c76d8eb2 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Wed Sep 11 15:49:39 2013 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Wed Sep 11 16:16:45 2013 +0200
@@ -1,5 +1,5 @@
-(*  Title:  HOL/ex/Adhoc_Overloading_Examples.thy
-    Author: Christian Sternagel
+(*  Title:      HOL/ex/Adhoc_Overloading_Examples.thy
+    Author:     Christian Sternagel
 *)
 
 header {* Ad Hoc Overloading *}
diff -r d0c163c6c725 -r 73d4c76d8eb2 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Provers/blast.ML	Wed Sep 11 16:16:45 2013 +0200
@@ -78,8 +78,8 @@
 (* options *)
 
 val (depth_limit, setup_depth_limit) = Attrib.config_int @{binding blast_depth_limit} (K 20);
-val (trace, setup_trace) = Attrib.config_bool @{binding blast_trace} (K false);
-val (stats, setup_stats) = Attrib.config_bool @{binding blast_stats} (K false);
+val (trace, _) = Attrib.config_bool @{binding blast_trace} (K false);
+val (stats, _) = Attrib.config_bool @{binding blast_stats} (K false);
 
 
 datatype term =
@@ -1298,8 +1298,6 @@
 
 val setup =
   setup_depth_limit #>
-  setup_trace #>
-  setup_stats #>
   Method.setup @{binding blast}
     (Scan.lift (Scan.option Parse.nat) --| Method.sections Classical.cla_modifiers >>
       (fn NONE => SIMPLE_METHOD' o blast_tac
diff -r d0c163c6c725 -r 73d4c76d8eb2 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Pure/General/name_space.ML	Wed Sep 11 16:16:45 2013 +0200
@@ -30,6 +30,7 @@
   val extern: Proof.context -> T -> string -> xstring
   val extern_ord: Proof.context -> T -> string * string -> order
   val markup_extern: Proof.context -> T -> string -> Markup.T * xstring
+  val pretty: Proof.context -> T -> string -> Pretty.T
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
   type naming
@@ -194,6 +195,8 @@
 
 fun markup_extern ctxt space name = (markup space name, extern ctxt space name);
 
+fun pretty ctxt space name = Pretty.mark_str (markup_extern ctxt space name);
+
 
 (* modify internals *)
 
diff -r d0c163c6c725 -r 73d4c76d8eb2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Pure/Isar/class.ML	Wed Sep 11 16:16:45 2013 +0200
@@ -182,14 +182,14 @@
 
     fun prt_param (c, ty) =
       Pretty.block
-       [Pretty.mark_str (Name_Space.markup_extern ctxt const_space c), Pretty.str " ::",
+       [Name_Space.pretty ctxt const_space c, Pretty.str " ::",
         Pretty.brk 1, Syntax.pretty_typ ctxt (Type.strip_sorts_dummy ty)];
 
     fun prt_entry class =
       Pretty.block
         ([Pretty.command "class", Pretty.brk 1,
-          Pretty.mark_str (Name_Space.markup_extern ctxt class_space class), Pretty.str ":",
-          Pretty.fbrk, Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
+          Name_Space.pretty ctxt class_space class, Pretty.str ":", Pretty.fbrk,
+          Pretty.block [Pretty.str "supersort: ", prt_supersort class]] @
           (case try (Axclass.get_info thy) class of
             NONE => []
           | SOME {params, ...} =>
diff -r d0c163c6c725 -r 73d4c76d8eb2 src/Tools/adhoc_overloading.ML
--- a/src/Tools/adhoc_overloading.ML	Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Tools/adhoc_overloading.ML	Wed Sep 11 16:16:45 2013 +0200
@@ -1,5 +1,5 @@
-(* Author: Alexander Krauss, TU Muenchen
-   Author: Christian Sternagel, University of Innsbruck
+(*  Author:     Alexander Krauss, TU Muenchen
+    Author:     Christian Sternagel, University of Innsbruck
 
 Adhoc overloading of constants based on their types.
 *)
@@ -21,6 +21,7 @@
 
 val show_variants = Attrib.setup_config_bool @{binding show_variants} (K false);
 
+
 (* errors *)
 
 fun err_duplicate_variant oconst =
@@ -32,19 +33,27 @@
 fun err_not_overloaded oconst =
   error ("Constant " ^ quote oconst ^ " is not declared as overloaded");
 
-fun err_unresolved_overloading ctxt (c, T) t instances =
-  let val ctxt' = Config.put show_variants true ctxt
+fun err_unresolved_overloading ctxt0 (c, T) t instances =
+  let
+    val ctxt = Config.put show_variants true ctxt0
+    val const_space = Proof_Context.const_space ctxt
+    val prt_const =
+      Pretty.block [Name_Space.pretty ctxt const_space c, Pretty.str " ::", Pretty.brk 1,
+        Pretty.quote (Syntax.pretty_typ ctxt T)]
   in
-    cat_lines (
-      "Unresolved overloading of constant" ::
-      quote c ^ " :: " ^ quote (Syntax.string_of_typ ctxt' T) ::
-      "in term " ::
-      quote (Syntax.string_of_term ctxt' t) ::
-      (if null instances then "no instances" else "multiple instances:") ::
-    map (Markup.markup Markup.item o Syntax.string_of_term ctxt') instances)
-    |> error
+    error (Pretty.string_of (Pretty.chunks [
+      Pretty.block [
+        Pretty.str "Unresolved adhoc overloading of constant", Pretty.brk 1,
+        prt_const, Pretty.brk 1, Pretty.str "in term", Pretty.brk 1,
+        Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t)]],
+      Pretty.block (
+        (if null instances then [Pretty.str "no instances"]
+        else Pretty.fbreaks (
+          Pretty.str "multiple instances:" ::
+          map (Pretty.mark Markup.item o Syntax.pretty_term ctxt) instances)))]))
   end;
 
+
 (* generic data *)
 
 fun variants_eq ((v1, T1), (v2, T2)) =
@@ -133,6 +142,7 @@
   val generic_remove_variant = generic_variant false;
 end;
 
+
 (* check / uncheck *)
 
 fun unifiable_with thy T1 T2 =
@@ -178,6 +188,7 @@
       | (cT :: _) => err_unresolved_overloading ctxt cT t (the_candidates cT));
   in map check_unresolved end;
 
+
 (* setup *)
 
 val _ = Context.>>
@@ -185,6 +196,7 @@
    #> Syntax_Phases.term_check 1 "adhoc_overloading_unresolved_check" reject_unresolved
    #> Syntax_Phases.term_uncheck 0 "adhoc_overloading" uncheck);
 
+
 (* commands *)
 
 fun generic_adhoc_overloading_cmd add =
diff -r d0c163c6c725 -r 73d4c76d8eb2 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Wed Sep 11 15:49:39 2013 +0200
+++ b/src/Tools/subtyping.ML	Wed Sep 11 16:16:45 2013 +0200
@@ -1046,9 +1046,9 @@
     val tmaps =
       sort (Name_Space.extern_ord ctxt type_space o pairself #1)
         (Symtab.dest (tmaps_of ctxt));
-    fun show_map (x, (t, _)) =
+    fun show_map (c, (t, _)) =
       Pretty.block
-       [Pretty.mark_str (Name_Space.markup_extern ctxt type_space x), Pretty.str ":",
+       [Name_Space.pretty ctxt type_space c, Pretty.str ":",
         Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt t)];
   in
    [Pretty.big_list "coercions between base types:" (map show_coercion simple),