tweaked signature
authorblanchet
Tue, 15 Oct 2013 23:00:46 +0200
changeset 54118 f5fc8525838f
parent 54117 32730ba3ab85
child 54119 2c13cb4a057d
tweaked signature
src/HOL/TPTP/MaSh_Export.thy
src/HOL/TPTP/mash_export.ML
--- 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)