| changeset 55212 | 5832470d956e |
| parent 55208 | 11dd3d1da83b |
| child 57120 | f8112c4b9cb8 |
--- a/src/HOL/TPTP/MaSh_Export.thy Fri Jan 31 16:07:20 2014 +0100 +++ b/src/HOL/TPTP/MaSh_Export.thy Fri Jan 31 16:10:39 2014 +0100 @@ -56,7 +56,7 @@ ML {* if do_it then - generate_features @{context} prover thys (prefix ^ "mash_features") + generate_features @{context} thys (prefix ^ "mash_features") else () *}