--- a/src/HOL/ex/SAT_Examples.thy Sun Mar 20 21:20:07 2011 +0100
+++ b/src/HOL/ex/SAT_Examples.thy Sun Mar 20 21:28:11 2011 +0100
@@ -536,13 +536,12 @@
fun and_to_list (Prop_Logic.And (fm1, fm2)) acc = and_to_list fm2 (fm1 :: acc)
| and_to_list fm acc = rev (fm :: acc)
val clauses = and_to_list prop_fm []
- val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula)
- clauses
- val cterms = map (Thm.cterm_of @{theory}) terms
- val timer = start_timing ()
- val thm = sat.rawsat_thm @{context} cterms
+ val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
+ val cterms = map (Thm.cterm_of @{theory}) terms
+ val start = Timing.start ()
+ val thm = sat.rawsat_thm @{context} cterms
in
- (end_timing timer, !sat.counter)
+ (Timing.result start, ! sat.counter)
end;
*}