# HG changeset patch # User blanchet # Date 1404226030 -7200 # Node ID 29efe682335be2e298041cac146701df3a7e28a0 # Parent 9cc802a8ab06c11871efb325ea0805d454916eef removed needless code diff -r 9cc802a8ab06 -r 29efe682335b src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jul 01 16:47:10 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Tue Jul 01 16:47:10 2014 +0200 @@ -541,7 +541,7 @@ val decode_str = String.explode #> unmeta_chars [] val encode_strs = map encode_str #> space_implode " " -val decode_strs = space_explode " " #> filter_out (curry (op =) "") #> map decode_str +val decode_strs = space_explode " " #> map decode_str datatype proof_kind = Isar_Proof | Automatic_Proof | Isar_Proof_wegen_Prover_Flop