merged

--- a/src/HOL/Library/code_test.ML	Sat Apr 11 22:19:09 2015 +0100
+++ b/src/HOL/Library/code_test.ML	Sat Apr 11 23:55:04 2015 +0200
@@ -148,7 +148,8 @@
        (ts ~~ evals))]
 
 fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
-  Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
+  Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for")
+    @ [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt query)]
     @ pretty_eval ctxt evals eval_ts)
 
 fun pretty_failures ctxt target failures =

--- a/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 11 22:19:09 2015 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Sat Apr 11 23:55:04 2015 +0200
@@ -330,13 +330,13 @@
 
     fun print_wf (x, (gfp, wf)) =
       pprint_nt (fn () => Pretty.blk (0,
-          Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate \"")
-          @ Syntax.pretty_term ctxt (Const x) ::
+          Pretty.text ("The " ^ (if gfp then "co" else "") ^ "inductive predicate") @
+          [Pretty.brk 1, Pretty.quote (Syntax.pretty_term ctxt (Const x)), Pretty.brk 1] @
           Pretty.text (if wf then
-                   "\" was proved well-founded. Nitpick can compute it \
+                   "was proved well-founded. Nitpick can compute it \
                    \efficiently."
                  else
-                   "\" could not be proved well-founded. Nitpick might need to \
+                   "could not be proved well-founded. Nitpick might need to \
                    \unroll it.")))
     val _ = if verbose then List.app print_wf (!wf_cache) else ()
     val das_wort_formula = if falsify then "Negated conjecture" else "Formula"
@@ -367,9 +367,9 @@
     fun monotonicity_message Ts extra =
       let val pretties = map (pretty_maybe_quote keywords o pretty_for_type ctxt) Ts in
         Pretty.blk (0,
-          Pretty.text ("The type" ^ plural_s_for_list pretties ^ " ") @
-          pretty_serial_commas "and" pretties @
-          Pretty.text (" " ^
+          Pretty.text ("The type" ^ plural_s_for_list pretties) @ [Pretty.brk 1] @
+          pretty_serial_commas "and" pretties @ [Pretty.brk 1] @
+          Pretty.text (
                  (if none_true monos then
                     "passed the monotonicity test"
                   else
@@ -664,7 +664,7 @@
                            else " quasi genuine ") ^ das_wort_model) @
                    (case pretties_for_scope scope verbose of
                       [] => []
-                    | pretties => Pretty.text " for " @ pretties) @
+                    | pretties => [Pretty.brk 1, Pretty.str "for", Pretty.brk 1] @ pretties) @
                    [Pretty.str ":", Pretty.fbrk])),
               Pretty.indent indent_size reconstructed_model]);
          print_t (K "% SZS output end FiniteModel");