changeset 55570 | f5fc8525838f |
parent 54257 | 43d5f3d6d04e |
child 56059 | 42c209a6c225 |
1.1 --- a/src/HOL/TPTP/MaSh_Export.thy Tue Oct 15 22:55:01 2013 +0200 1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy Tue Oct 15 23:00:46 2013 +0200 1.3 @@ -63,7 +63,7 @@ 1.4 1.5 ML {* 1.6 if do_it then 1.7 - generate_isar_dependencies @{context} thys linearize 1.8 + generate_isar_dependencies @{context} range thys linearize 1.9 (prefix ^ "mash_dependencies") 1.10 else 1.11 ()