Avoid ML warning about unreferenced identifier.
authorwebertj
Tue Mar 05 13:03:24 2013 +0100 (2013-03-05)
changeset 513371012626af0bc
parent 51336 6c06b8de72f9
child 51339 04ebef4ee844
Avoid ML warning about unreferenced identifier.
src/HOL/ex/SAT_Examples.thy
     1.1 --- a/src/HOL/ex/SAT_Examples.thy	Tue Mar 05 11:59:58 2013 +0100
     1.2 +++ b/src/HOL/ex/SAT_Examples.thy	Tue Mar 05 13:03:24 2013 +0100
     1.3 @@ -535,7 +535,7 @@
     1.4    val terms = map (HOLogic.mk_Trueprop o Prop_Logic.term_of_prop_formula) clauses
     1.5    val cterms = map (Thm.cterm_of @{theory}) terms
     1.6    val start = Timing.start ()
     1.7 -  val thm = sat.rawsat_thm @{context} cterms
     1.8 +  val _ = sat.rawsat_thm @{context} cterms
     1.9  in
    1.10    (Timing.result start, ! sat.counter)
    1.11  end;