# HG changeset patch
# User blanchet
# Date 1311684780 -7200
# Node ID 33d8b99531c2c8a84f0907fdc23b29208f425356
# Parent  aefc5b046c1e5c86d2ab10d752b773b74002e525
no need for existential witnesses for sorts in TFF and THF formats

diff -r aefc5b046c1e -r 33d8b99531c2 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 26 14:53:00 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 26 14:53:00 2011 +0200
@@ -1696,7 +1696,9 @@
     |> is_type_enc_fairly_sound type_enc
        ? (fold (add_fact_syms true) conjs
           #> fold (add_fact_syms false) facts
-          #> fold add_undefined_const (var_types ()))
+          #> (case type_enc of
+                Simple_Types _ => I
+              | _ => fold add_undefined_const (var_types ())))
   end
 
 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it