# HG changeset patch
# User wenzelm
# Date 1254420284 -7200
# Node ID f3716d1a2e48a948755d0567f98017ebaf5fa6e1
# Parent  2729c803332628a86e0b845031fb3f2ce61be650
explicitly Unsynchronized;

diff -r 2729c8033326 -r f3716d1a2e48 doc-src/Codegen/Thy/Setup.thy
--- a/doc-src/Codegen/Thy/Setup.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/Codegen/Thy/Setup.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -10,6 +10,6 @@
    "~~/src/HOL/Decision_Procs/Ferrack"] *}
 
 ML_command {* Code_Target.code_width := 74 *}
-ML_command {* reset unique_names *}
+ML_command {* Unsynchronized.reset unique_names *}
 
 end
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/IsarImplementation/Thy/Integration.thy
--- a/doc-src/IsarImplementation/Thy/Integration.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Integration.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -59,9 +59,9 @@
   @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\
   @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\
   @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\
-  @{index_ML Toplevel.debug: "bool ref"} \\
-  @{index_ML Toplevel.timing: "bool ref"} \\
-  @{index_ML Toplevel.profiling: "int ref"} \\
+  @{index_ML Toplevel.debug: "bool Unsynchronized.ref"} \\
+  @{index_ML Toplevel.timing: "bool Unsynchronized.ref"} \\
+  @{index_ML Toplevel.profiling: "int Unsynchronized.ref"} \\
   \end{mldecls}
 
   \begin{description}
@@ -85,11 +85,11 @@
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "set Toplevel.debug"} makes the toplevel print further
+  \item @{ML "Toplevel.debug := true"} makes the toplevel print further
   details about internal error conditions, exceptions being raised
   etc.
 
-  \item @{ML "set Toplevel.timing"} makes the toplevel print timing
+  \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.
 
   \item @{ML Toplevel.profiling}~@{verbatim ":="}~@{text "n"} controls
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -547,7 +547,7 @@
   \end{mldecls}
   \begin{mldecls}
   @{index_ML_type thm} \\
-  @{index_ML proofs: "int ref"} \\
+  @{index_ML proofs: "int Unsynchronized.ref"} \\
   @{index_ML Thm.assume: "cterm -> thm"} \\
   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/IsarImplementation/Thy/ML.thy
--- a/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -258,7 +258,7 @@
   \begin{mldecls}
   @{index_ML NAMED_CRITICAL: "string -> (unit -> 'a) -> 'a"} \\
   @{index_ML CRITICAL: "(unit -> 'a) -> 'a"} \\
-  @{index_ML setmp: "'a ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
+  @{index_ML setmp: "'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c"} \\
   \end{mldecls}
 
   \begin{description}
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -96,19 +96,19 @@
 
 text {*
   \begin{mldecls} 
-    @{index_ML show_types: "bool ref"} & default @{ML false} \\
-    @{index_ML show_sorts: "bool ref"} & default @{ML false} \\
-    @{index_ML show_consts: "bool ref"} & default @{ML false} \\
-    @{index_ML long_names: "bool ref"} & default @{ML false} \\
-    @{index_ML short_names: "bool ref"} & default @{ML false} \\
-    @{index_ML unique_names: "bool ref"} & default @{ML true} \\
-    @{index_ML show_brackets: "bool ref"} & default @{ML false} \\
-    @{index_ML eta_contract: "bool ref"} & default @{ML true} \\
-    @{index_ML goals_limit: "int ref"} & default @{ML 10} \\
-    @{index_ML Proof.show_main_goal: "bool ref"} & default @{ML false} \\
-    @{index_ML show_hyps: "bool ref"} & default @{ML false} \\
-    @{index_ML show_tags: "bool ref"} & default @{ML false} \\
-    @{index_ML show_question_marks: "bool ref"} & default @{ML true} \\
+    @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_consts: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
+    @{index_ML show_brackets: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML eta_contract: "bool Unsynchronized.ref"} & default @{ML true} \\
+    @{index_ML goals_limit: "int Unsynchronized.ref"} & default @{ML 10} \\
+    @{index_ML Proof.show_main_goal: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_hyps: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_tags: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_question_marks: "bool Unsynchronized.ref"} & default @{ML true} \\
   \end{mldecls}
 
   These global ML variables control the detail of information that is
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/IsarRef/Thy/ROOT-HOLCF.ML
--- a/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-HOLCF.ML	Thu Oct 01 20:04:44 2009 +0200
@@ -1,4 +1,4 @@
-set ThyOutput.source;
+Unsynchronized.set ThyOutput.source;
 use "../../antiquote_setup.ML";
 
 use_thy "HOLCF_Specific";
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/IsarRef/Thy/ROOT-ZF.ML
--- a/doc-src/IsarRef/Thy/ROOT-ZF.ML	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/IsarRef/Thy/ROOT-ZF.ML	Thu Oct 01 20:04:44 2009 +0200
@@ -1,4 +1,4 @@
-set ThyOutput.source;
+Unsynchronized.set ThyOutput.source;
 use "../../antiquote_setup.ML";
 
 use_thy "ZF_Specific";
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/IsarRef/Thy/ROOT.ML
--- a/doc-src/IsarRef/Thy/ROOT.ML	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/IsarRef/Thy/ROOT.ML	Thu Oct 01 20:04:44 2009 +0200
@@ -1,5 +1,5 @@
-set quick_and_dirty;
-set ThyOutput.source;
+Unsynchronized.set quick_and_dirty;
+Unsynchronized.set ThyOutput.source;
 use "../../antiquote_setup.ML";
 
 use_thys [
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/LaTeXsugar/Sugar/Sugar.thy
--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -143,7 +143,7 @@
 internal index. This can be avoided by turning the last digit into a
 subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *}
 
-(*<*)ML"reset show_question_marks"(*>*)
+(*<*)ML"Unsynchronized.reset show_question_marks"(*>*)
 
 subsection {*Qualified names*}
 
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/System/Thy/ROOT.ML
--- a/doc-src/System/Thy/ROOT.ML	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/System/Thy/ROOT.ML	Thu Oct 01 20:04:44 2009 +0200
@@ -1,7 +1,4 @@
-set ThyOutput.source;
+Unsynchronized.set ThyOutput.source;
 use "../../antiquote_setup.ML";
 
-use_thy "Basics";
-use_thy "Interfaces";
-use_thy "Presentation";
-use_thy "Misc";
+use_thys ["Basics", "Interfaces", "Presentation", "Misc"];
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/TutorialI/Misc/Itrev.thy
--- a/doc-src/TutorialI/Misc/Itrev.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -2,7 +2,7 @@
 theory Itrev
 imports Main
 begin
-ML"reset NameSpace.unique_names"
+ML"Unsynchronized.reset NameSpace.unique_names"
 (*>*)
 
 section{*Induction Heuristics*}
@@ -141,6 +141,6 @@
 \index{induction heuristics|)}
 *}
 (*<*)
-ML"set NameSpace.unique_names"
+ML"Unsynchronized.set NameSpace.unique_names"
 end
 (*>*)
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/TutorialI/Rules/Basic.thy
--- a/doc-src/TutorialI/Rules/Basic.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/TutorialI/Rules/Basic.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -188,7 +188,7 @@
 
 text{*unification failure trace *}
 
-ML "set trace_unify_fail"
+ML "Unsynchronized.set trace_unify_fail"
 
 lemma "P(a, f(b, g(e,a), b), a) \<Longrightarrow> P(a, f(b, g(c,a), b), a)"
 txt{*
@@ -213,7 +213,7 @@
 *}
 oops
 
-ML "reset trace_unify_fail"
+ML "Unsynchronized.reset trace_unify_fail"
 
 
 text{*Quantifiers*}
diff -r 2729c8033326 -r f3716d1a2e48 doc-src/TutorialI/Sets/Examples.thy
--- a/doc-src/TutorialI/Sets/Examples.thy	Thu Oct 01 18:59:26 2009 +0200
+++ b/doc-src/TutorialI/Sets/Examples.thy	Thu Oct 01 20:04:44 2009 +0200
@@ -1,7 +1,7 @@
 (* ID:         $Id$ *)
 theory Examples imports Main Binomial begin
 
-ML "reset eta_contract"
+ML "Unsynchronized.reset eta_contract"
 ML "Pretty.setmargin 64"
 
 text{*membership, intersection *}