# HG changeset patch
# User wenzelm
# Date 1255789994 -7200
# Node ID 1df87354c3081665ea92a93751d146e3d3b0c177
# Parent  5b21661fe618353ba340a09dc580528816606410
Unsynchronized.set etc.;

diff -r 5b21661fe618 -r 1df87354c308 src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Sat Oct 17 15:57:51 2009 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Sat Oct 17 16:33:14 2009 +0200
@@ -7,13 +7,12 @@
 header {* Examples for the 'sat' and 'satx' tactic *}
 
 theory SAT_Examples imports Main
-
 begin
 
 (* ML {* sat.solver := "zchaff_with_proofs"; *} *)
 (* ML {* sat.solver := "minisat_with_proofs"; *} *)
-ML {* set sat.trace_sat; *}
-ML {* set quick_and_dirty; *}
+ML {* Unsynchronized.set sat.trace_sat; *}
+ML {* Unsynchronized.set quick_and_dirty; *}
 
 lemma "True"
 by sat
@@ -79,8 +78,8 @@
 lemma "(ALL x. P x) | ~ All P"
 by sat
 
-ML {* reset sat.trace_sat; *}
-ML {* reset quick_and_dirty; *}
+ML {* Unsynchronized.reset sat.trace_sat; *}
+ML {* Unsynchronized.reset quick_and_dirty; *}
 
 method_setup rawsat =
   {* Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac) *}