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