# HG changeset patch
# User ballarin
# Date 1257198682 -3600
# Node ID afaa9538e82cd648bd80b38a413857efec1f7f56
# Parent  6c273b0e0e26471d0dd7ef012b3cb0a6e6aa06d1
Make output indenpendent of current print mode.

diff -r 6c273b0e0e26 -r afaa9538e82c src/FOL/ex/LocaleTest.thy
--- a/src/FOL/ex/LocaleTest.thy	Mon Nov 02 21:27:26 2009 +0100
+++ b/src/FOL/ex/LocaleTest.thy	Mon Nov 02 22:51:22 2009 +0100
@@ -146,12 +146,14 @@
 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} <>
- "\^E\^Fterm\^E\^E\^Fconst\^Fname=local.d1\^Ed1\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E) <-> ~ \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E(\^E\^Ffixed\^Fname=p1\^E\^E\^Ffree\^Ep1\^E\^F\^E\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E))\^E\^F\^E" 
+ "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} <>
- "\^E\^Fterm\^E\^E\^Fconst\^Fname=local.d2\^Ed2\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E) <-> ~ \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E)\^E\^F\^E"
+ "d2(?x) <-> ~ p2(?x)"
 then error "Theorem syntax 'd2(?x) <-> ~ p2(?x)' expected." else ();
+print_mode := print_mode'
 *}
 
 end
@@ -163,13 +165,15 @@
   (* 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} <>
- "\^E\^Fterm\^E\^E\^Fconst\^Fname=LocaleTest.syntax.d1\^Esyntax.d1\^E\^F\^E(\^E\^Ffixed\^Fname=p3\^E\^E\^Ffree\^Ep3\^E\^F\^E\^E\^F\^E, \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E, \^E\^Fvar\^E?x\^E\^F\^E) <-> ~ \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E(\^E\^Ffixed\^Fname=p3\^E\^E\^Ffree\^Ep3\^E\^F\^E\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E))\^E\^F\^E"
+ "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} <>
- "\^E\^Fterm\^E\^E\^Fconst\^Fname=local.d2\^Ed2\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E) <-> ~ \^E\^Ffixed\^Fname=p2\^E\^E\^Ffree\^Ep2\^E\^F\^E\^E\^F\^E(\^E\^Fvar\^E?x\^E\^F\^E)\^E\^F\^E"
+ "d2(?x) <-> ~ p2(?x)"
 then error "Theorem syntax 'd2(?x) <-> ~ p2(?x)' expected." else ();
+print_mode := print_mode'
 *}
 
 end