--- a/src/HOL/Probability/measurable.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/HOL/Probability/measurable.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -204,7 +204,7 @@
 fun measurable_tac ctxt facts =
   let
     fun debug_fact msg thm () =
-      msg ^ " " ^ Pretty.str_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
+      msg ^ " " ^ Pretty.unformatted_string_of (Syntax.pretty_term ctxt (Thm.prop_of thm))
 
     fun IF' c t i = COND (c i) (t i) no_tac