# HG changeset patch
# User blanchet
# Date 1308141401 -7200
# Node ID 3d03f44728832b1395e324c3578b54d8dc632280
# Parent  5b499c360df6bdaabb4855bf98deef951f6d09db
use more appropriate type systems for ATP exporter

diff -r 5b499c360df6 -r 3d03f4472883 src/HOL/ex/ATP_Export.thy
--- a/src/HOL/ex/ATP_Export.thy	Wed Jun 15 14:36:41 2011 +0200
+++ b/src/HOL/ex/ATP_Export.thy	Wed Jun 15 14:36:41 2011 +0200
@@ -4,23 +4,31 @@
 begin
 
 ML {*
-val do_it = false; (* switch to true to generate files *)
+val do_it = false; (* switch to "true" to generate files *)
 val thy = @{theory Complex_Main};
 val ctxt = @{context}
 *}
 
 ML {*
 if do_it then
-  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy true
-      "/tmp/infs_full_types.tptp"
+  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_preds"
+      "/tmp/infs_poly_preds.tptp"
 else
   ()
 *}
 
 ML {*
 if do_it then
-  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy false
-      "/tmp/infs_partial_types.tptp"
+  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags"
+      "/tmp/infs_poly_tags.tptp"
+else
+  ()
+*}
+
+ML {*
+if do_it then
+  ATP_Export.generate_tptp_inference_file_for_theory ctxt thy "poly_tags_heavy"
+      "/tmp/infs_poly_tags_heavy.tptp"
 else
   ()
 *}
diff -r 5b499c360df6 -r 3d03f4472883 src/HOL/ex/atp_export.ML
--- a/src/HOL/ex/atp_export.ML	Wed Jun 15 14:36:41 2011 +0200
+++ b/src/HOL/ex/atp_export.ML	Wed Jun 15 14:36:41 2011 +0200
@@ -11,7 +11,7 @@
   val generate_tptp_graph_file_for_theory :
     Proof.context -> theory -> string -> unit
   val generate_tptp_inference_file_for_theory :
-    Proof.context -> theory -> bool -> string -> unit
+    Proof.context -> theory -> string -> string -> unit
 end;
 
 structure ATP_Export : ATP_EXPORT =
@@ -87,15 +87,10 @@
 val add_inferences_to_problem =
   map o apsnd o map o add_inferences_to_problem_line
 
-fun generate_tptp_inference_file_for_theory ctxt thy full_types file_name =
+fun generate_tptp_inference_file_for_theory ctxt thy type_sys file_name =
   let
     val format = ATP_Problem.FOF
-    val type_sys =
-      ATP_Translate.Preds
-          (ATP_Translate.Polymorphic,
-           if full_types then ATP_Translate.All_Types
-           else ATP_Translate.Const_Arg_Types,
-           ATP_Translate.Heavyweight)
+    val type_sys = type_sys |> ATP_Translate.type_sys_from_string
     val path = file_name |> Path.explode
     val _ = File.write path ""
     val facts0 = facts_of thy