Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML
changeset 57243 8c261f0a9b32
parent 57078 a91d126338a4 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Jun 12 17:02:03 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML	Thu Jun 12 17:02:03 2014 +0200
@@ -71,7 +71,7 @@
 
 fun weight_smt_fact ctxt num_facts ((info, th), j) =
   let val thy = Proof_Context.theory_of ctxt in
-    (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th (* TODO: needed? *)))
+    (info, (smt_fact_weight ctxt j num_facts, Thm.transfer thy th))
   end
 
 (* "SMT_Failure.Abnormal_Termination" carries the solver's return code. Until these are sorted out
isabelle