--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Mar 10 21:40:39 2014 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Mon Mar 10 21:58:54 2014 +0100
@@ -150,7 +150,8 @@
ML {*
fun check_syntax ctxt thm expected =
let
- val obtained = Print_Mode.setmp [] (Display.string_of_thm ctxt) thm;
+ val obtained =
+ Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm;
in
if obtained <> expected
then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")