src/HOL/TPTP/MaSh_Export.thy
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    ()