--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:22:17 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Nov 28 12:23:44 2012 +0100
@@ -478,7 +478,6 @@
(Syntax.string_of_typ ctxt) T))
fun do_label l = if l = no_label then "" else string_for_label l ^ ": "
fun do_have qs =
- (if member (op =) qs Moreover then "moreover " else "") ^
(if member (op =) qs Ultimately then "ultimately " else "") ^
(if member (op =) qs Then then
if member (op =) qs Show then "thus" else "hence"