author | blanchet |
Fri, 01 Oct 2010 18:48:37 +0200 | |
changeset 39908 | 44cd24da1beb |
parent 39907 | b0be1daf0667 |
child 39909 | b93f27358100 |
--- a/src/HOL/Tools/Sledgehammer/meson_clausify.ML Fri Oct 01 17:56:32 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/meson_clausify.ML Fri Oct 01 18:48:37 2010 +0200 @@ -340,7 +340,7 @@ |>> the_single |>> cterm_of thy in (SOME (discharger_th, ct), Thm.assume ct, ctxt) end else - (NONE, th, ctxt) + (NONE, th, ctxt) end else (NONE, th, ctxt)