
diff -r 387dc978422b -r 2f970c7f722b src/HOL/ex/SAT_Examples.thy
--- a/src/HOL/ex/SAT_Examples.thy	Fri May 17 20:30:04 2013 +0200
+++ b/src/HOL/ex/SAT_Examples.thy	Fri May 17 20:41:45 2013 +0200
@@ -11,7 +11,7 @@
 (* ML {* sat.solver := "zchaff_with_proofs"; *} *)
 (* ML {* sat.solver := "minisat_with_proofs"; *} *)
 ML {* sat.trace_sat := true; *}
-ML {* quick_and_dirty := true; *}
+declare [[quick_and_dirty]]
 
 lemma "True"
 by sat
@@ -78,7 +78,7 @@
 by sat
 
 ML {* sat.trace_sat := false; *}
-ML {* quick_and_dirty := false; *}
+declare [[quick_and_dirty = false]]
 
 method_setup rawsat = {*
   Scan.succeed (SIMPLE_METHOD' o sat.rawsat_tac)
@@ -522,8 +522,9 @@
 (* ML {*
 sat.solver := "zchaff_with_proofs";
 sat.trace_sat := false;
-quick_and_dirty := false;
-*} *)
+*}
+declare [[quick_and_dirty = false]]
+*)
 
 ML {*
 fun benchmark dimacsfile =




