| author | webertj |
| Tue, 05 Mar 2013 13:03:24 +0100 | |
| changeset 51337 | 1012626af0bc |
| parent 51336 | 6c06b8de72f9 |
| child 51339 | 04ebef4ee844 |
--- a/src/HOL/ex/SAT_Examples.thy Tue Mar 05 11:59:58 2013 +0100 +++ b/src/HOL/ex/SAT_Examples.thy Tue Mar 05 13:03:24 2013 +0100 @@ -535,7 +535,7 @@ 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 + val _ = sat.rawsat_thm @{context} cterms in (Timing.result start, ! sat.counter) end;