# HG changeset patch
# User blanchet
# Date 1363790135 -3600
# Node ID 60472a1b4536ce2b1fd27fdb8f00d3036bd0457c
# Parent  d53cdbca1be4405d6ebcdd3ad0d249f9d0ef84f7
use the right role for SPASS hypotheses

diff -r d53cdbca1be4 -r 60472a1b4536 src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Mar 20 14:56:30 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Wed Mar 20 15:35:35 2013 +0100
@@ -608,12 +608,12 @@
 
 (* Not really a prover: Experimental Polymorphic THF and DFG output *)
 
-fun dummy_config format type_enc : atp_config =
+fun dummy_config prem_role format type_enc : atp_config =
   {exec = (["ISABELLE_ATP"], ["scripts/dummy_atp"]),
    arguments = K (K (K (K (K (K ""))))),
    proof_delims = [],
    known_failures = known_szs_status_failures,
-   prem_role = Hypothesis,
+   prem_role = prem_role,
    best_slices =
      K [(1.0, (((200, ""), format, type_enc,
                 if is_format_higher_order format then keep_lamsN
@@ -623,11 +623,13 @@
 
 val dummy_thf_format =
   THF (Polymorphic, TPTP_Explicit, THF_With_Choice, THF_With_Defs)
-val dummy_thf_config = dummy_config dummy_thf_format "poly_native_higher"
+val dummy_thf_config =
+  dummy_config Hypothesis dummy_thf_format "poly_native_higher"
 val dummy_thf = (dummy_thfN, fn () => dummy_thf_config)
 
 val spass_poly_format = DFG Polymorphic
-val spass_poly_config = dummy_config spass_poly_format "tc_native"
+val spass_poly_config =
+  dummy_config (#prem_role spass_config) spass_poly_format "tc_native"
 val spass_poly = (spass_polyN, fn () => spass_poly_config)
 
 (* Remote ATP invocation via SystemOnTPTP *)