--- 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
()
--- a/src/HOL/TPTP/mash_export.ML Tue Oct 15 22:55:01 2013 +0200
+++ b/src/HOL/TPTP/mash_export.ML Tue Oct 15 23:00:46 2013 +0200
@@ -14,7 +14,7 @@
val generate_features :
Proof.context -> string -> theory list -> string -> unit
val generate_isar_dependencies :
- Proof.context -> theory list -> bool -> string -> unit
+ Proof.context -> int * int option -> theory list -> bool -> string -> unit
val generate_prover_dependencies :
Proof.context -> params -> int * int option -> theory list -> bool -> string
-> unit
@@ -134,7 +134,7 @@
in File.write_list path lines end
fun generate_isar_dependencies ctxt =
- generate_isar_or_prover_dependencies ctxt NONE (1, NONE)
+ generate_isar_or_prover_dependencies ctxt NONE
fun generate_prover_dependencies ctxt params =
generate_isar_or_prover_dependencies ctxt (SOME params)