avoid unsynchronized refs within theory sources;

--- a/doc-src/IsarOverview/Isar/Logic.thy	Thu Oct 01 20:04:44 2009 +0200
+++ b/doc-src/IsarOverview/Isar/Logic.thy	Thu Oct 01 20:06:11 2009 +0200
@@ -526,7 +526,6 @@
 tendency to use the default introduction and elimination rules to
 decompose goals and facts. This can lead to very tedious proofs:
 *}
-(*<*)ML"set quick_and_dirty"(*>*)
 lemma "\<forall>x y. A x y \<and> B x y \<longrightarrow> C x y"
 proof
   fix x show "\<forall>y. A x y \<and> B x y \<longrightarrow> C x y"

--- a/doc-src/IsarOverview/Isar/ROOT.ML	Thu Oct 01 20:04:44 2009 +0200
+++ b/doc-src/IsarOverview/Isar/ROOT.ML	Thu Oct 01 20:06:11 2009 +0200
@@ -1,2 +1,3 @@
-use_thy "Logic";
-use_thy "Induction"
+Unsynchronized.set quick_and_dirty;
+
+use_thys ["Logic", "Induction"];

--- a/doc-src/TutorialI/Types/Numbers.thy	Thu Oct 01 20:04:44 2009 +0200
+++ b/doc-src/TutorialI/Types/Numbers.thy	Thu Oct 01 20:06:11 2009 +0200
@@ -252,18 +252,13 @@
 \rulename{mult_cancel_left}
 *}
 
-ML{*set show_sorts*}
-
 text{*
 effect of show sorts on the above
 
-@{thm[display] mult_cancel_left[no_vars]}
+@{thm[display,show_sorts] mult_cancel_left[no_vars]}
 \rulename{mult_cancel_left}
 *}
 
-ML{*reset show_sorts*}
-
-
 text{*
 absolute value