# 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