enabled test in PIDE interaction;
authorwenzelm
Mon Mar 10 21:58:54 2014 +0100 (2014-03-10)
changeset 560366c3fc3b5592a
parent 56035 745f568837f1
child 56037 7b716baac02c
enabled test in PIDE interaction;
src/FOL/ex/Locale_Test/Locale_Test1.thy
     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.")