src/FOL/ex/Locale_Test/Locale_Test1.thy
changeset 56036 6c3fc3b5592a
parent 55380 4de48353034e
child 56138 f42de6d8ed8e
     1.1 --- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Mar 10 21:40:39 2014 +0100
     1.2 +++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Mar 10 21:58:54 2014 +0100
     1.3 @@ -150,7 +150,8 @@
     1.4  ML {*
     1.5    fun check_syntax ctxt thm expected =
     1.6      let
     1.7 -      val obtained = Print_Mode.setmp [] (Display.string_of_thm ctxt) thm;
     1.8 +      val obtained =
     1.9 +        Print_Mode.setmp [] (Display.string_of_thm (Config.put show_markup false ctxt)) thm;
    1.10      in
    1.11        if obtained <> expected
    1.12        then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")