# HG changeset patch
# User blanchet
# Date 1381870846 -7200
# Node ID f5fc8525838fd6583f0d2e0f7e0e538764c9d38a
# Parent  32730ba3ab850e621ef0ee8e703d2024aef9b976
tweaked signature

diff -r 32730ba3ab85 -r f5fc8525838f src/HOL/TPTP/MaSh_Export.thy
--- 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
   ()
diff -r 32730ba3ab85 -r f5fc8525838f src/HOL/TPTP/mash_export.ML
--- 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)