diff -r 97921d23ebe3 -r efc4c0e0e14a src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Sat Feb 01 21:09:53 2014 +0100
+++ b/src/HOL/ex/SAT_Examples.thy	Sat Feb 01 21:43:23 2014 +0100
@@ -3,14 +3,17 @@
     Copyright   2005-2009
 *)
 
-header {* Examples for the 'sat' and 'satx' tactic *}
+header {* Examples for proof methods "sat" and "satx" *}
 
 theory SAT_Examples imports Main
 begin
 
-(* ML {* SAT.solver := "zchaff_with_proofs"; *} *)
-(* ML {* SAT.solver := "minisat_with_proofs"; *} *)
-ML {* SAT.trace_sat := true; *}
+(*
+declare [[sat_solver = zchaff_with_proofs]]
+declare [[sat_solver = minisat_with_proofs]]
+*)
+
+declare [[sat_trace]]
 declare [[quick_and_dirty]]
 
 lemma "True"
@@ -24,13 +27,13 @@
 
 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
 (*
-apply (tactic {* CNF.cnf_rewrite_tac 1 *})
+apply (tactic {* CNF.cnf_rewrite_tac @{context} 1 *})
 *)
 by sat
 
 lemma "(a & b) | (c & d) \<Longrightarrow> (a & b) | (c & d)"
 (*
-apply (tactic {* CNF.cnfx_rewrite_tac 1 *})
+apply (tactic {* CNF.cnfx_rewrite_tac @{context} 1 *})
 apply (erule exE | erule conjE)+
 *)
 by satx
@@ -38,14 +41,14 @@
 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
   \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
 (*
-apply (tactic {* CNF.cnf_rewrite_tac 1 *})
+apply (tactic {* CNF.cnf_rewrite_tac @{context} 1 *})
 *)
 by sat
 
 lemma "(a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)
   \<Longrightarrow> (a & b | c & d) & (e & f | g & h) | (i & j | k & l) & (m & n | p & q)"
 (*
-apply (tactic {* CNF.cnfx_rewrite_tac 1 *})
+apply (tactic {* CNF.cnfx_rewrite_tac @{context} 1 *})
 apply (erule exE | erule conjE)+
 *)
 by satx
@@ -77,7 +80,7 @@
 lemma "(ALL x. P x) | ~ All P"
 by sat
 
-ML {* SAT.trace_sat := false; *}
+declare [[sat_trace = false]]
 declare [[quick_and_dirty = false]]
 
 method_setup rawsat = {*
@@ -519,13 +522,11 @@
 the number of resolution steps in the proof.
 *}
 
-(* ML {*
-SAT.solver := "zchaff_with_proofs";
-SAT.trace_sat := false;
-*}
+(*
+declare [[sat_solver = zchaff_with_proofs]]
+declare [[sat_trace = false]]
 declare [[quick_and_dirty = false]]
 *)
-
 ML {*
   fun benchmark dimacsfile =
     let