# HG changeset patch
# User wenzelm
# Date 1394485134 -3600
# Node ID 6c3fc3b5592ab60bdbaab9167d1570355eee512c
# Parent  745f568837f18f8e50be0051e11ddf9220d01941
enabled test in PIDE interaction;

diff -r 745f568837f1 -r 6c3fc3b5592a src/FOL/ex/Locale_Test/Locale_Test1.thy
--- 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.")