Avoid ML warning about unreferenced identifier.
authorwebertj
Tue, 05 Mar 2013 13:03:24 +0100
changeset 51337 1012626af0bc
parent 51336 6c06b8de72f9
child 51339 04ebef4ee844
Avoid ML warning about unreferenced identifier.
src/HOL/ex/SAT_Examples.thy
--- 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;