# HG changeset patch
# User blanchet
# Date 1452514515 -3600
# Node ID 2d187ace28274b8d7896a15a1128a8651801d7f1
# Parent  438f5986d11c3ef26165ffbc4a2a425101cb7066
avoid generating TFF1 or polymorphic DFG constructs in Vampire or SPASS problems for goals containing schematic type variables

diff -r 438f5986d11c -r 2d187ace2827 src/HOL/Tools/ATP/atp_problem_generate.ML
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jan 11 13:15:14 2016 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Mon Jan 11 13:15:15 2016 +0100
@@ -1216,8 +1216,8 @@
            lambda_ts (1 upto length lambda_ts)
   in (facts, lam_facts) end
 
-(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate the
-   same in Sledgehammer to prevent the discovery of unreplayable proofs. *)
+(* Metis's use of "resolve_tac" freezes the schematic variables. We simulate this in Sledgehammer to
+   prevent the discovery of unreplayable proofs. *)
 fun freeze_term t =
   let
     (* Freshness is desirable for completeness, but not for soundness. *)
@@ -1841,10 +1841,13 @@
     (* Remove existing facts from the conjecture, as this can dramatically boost an ATP's
        performance (for some reason). *)
     val hyp_ts = hyp_ts |> map (fn t => if member (op aconv) fact_ts t then @{prop True} else t)
+
+    val hyp_ts = map freeze_term hyp_ts;
+    val concl_t = freeze_term concl_t;
+
     val facts = facts |> map (apsnd (pair Axiom))
     val conjs =
       map (pair prem_role) hyp_ts @ [(Conjecture, s_not_prop concl_t)]
-      |> map (apsnd freeze_term)
       |> map2 (pair o rpair (Local, General) o string_of_int) (0 upto length hyp_ts)
     val ((conjs, facts), lam_facts) =
       (conjs, facts)