# HG changeset patch
# User ballarin
# Date 1257371487 -3600
# Node ID ddcf2004e215a7fdf5ac861cbb9d1140dc82a33b
# Parent  afaa9538e82cd648bd80b38a413857efec1f7f56
Use PrintMode.setmp to make thread-safe; avoid code clones.

diff -r afaa9538e82c -r ddcf2004e215 src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Mon Nov 02 22:51:22 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Wed Nov 04 22:51:27 2009 +0100
@@ -146,14 +146,19 @@
 thm d1_def d2_def  (* should print as "d1(?x) <-> ..." and "d2(?x) <-> ..." *)
 
 ML {*
-val print_mode' = print_mode_value (); print_mode := [];
-if Display.string_of_thm @{context} @{thm d1_def} <>
- "d1(?x) <-> ~ p2(p1(?x))" 
-then error "Theorem syntax 'd1(?x) <-> ~ p2(p1(?x))' expected." else ();
-if Display.string_of_thm @{context} @{thm d2_def} <>
- "d2(?x) <-> ~ p2(?x)"
-then error "Theorem syntax 'd2(?x) <-> ~ p2(?x)' expected." else ();
-print_mode := print_mode'
+  fun check_syntax ctxt thm expected =
+    let
+      val obtained = PrintMode.setmp [] (Display.string_of_thm ctxt) thm;
+    in
+      if obtained <> expected
+      then error ("Theorem syntax '" ^ obtained ^ "' obtained, but '" ^ expected ^ "' expected.")
+      else ()
+    end;
+*}
+
+ML {*
+  check_syntax @{context} @{thm d1_def} "d1(?x) <-> ~ p2(p1(?x))";
+  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
 *}
 
 end
@@ -165,15 +170,8 @@
   (* should print as "syntax.d1(p3, p2, ?x) <-> ..." and "d2(?x) <-> ..." *)
 
 ML {*
-val print_mode' = print_mode_value (); print_mode := [];
-if Display.string_of_thm @{context} @{thm d1_def} <>
- "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))"
-then error "Theorem syntax 'syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))' expected."
-else ();
-if Display.string_of_thm @{context} @{thm d2_def} <>
- "d2(?x) <-> ~ p2(?x)"
-then error "Theorem syntax 'd2(?x) <-> ~ p2(?x)' expected." else ();
-print_mode := print_mode'
+  check_syntax @{context} @{thm d1_def} "syntax.d1(p3, p2, ?x) <-> ~ p2(p3(?x))";
+  check_syntax @{context} @{thm d2_def} "d2(?x) <-> ~ p2(?x)";
 *}
 
 end