changeset 54118 | f5fc8525838f |
parent 53120 | 43d5f3d6d04e |
child 54717 | 42c209a6c225 |
--- a/src/HOL/TPTP/MaSh_Export.thy Tue Oct 15 22:55:01 2013 +0200 +++ b/src/HOL/TPTP/MaSh_Export.thy Tue Oct 15 23:00:46 2013 +0200 @@ -63,7 +63,7 @@ ML {* if do_it then - generate_isar_dependencies @{context} thys linearize + generate_isar_dependencies @{context} range thys linearize (prefix ^ "mash_dependencies") else ()