1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 26 14:53:00 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Tue Jul 26 14:53:00 2011 +0200
     1.3 @@ -1696,7 +1696,9 @@
     1.4      |> is_type_enc_fairly_sound type_enc
     1.5         ? (fold (add_fact_syms true) conjs
     1.6            #> fold (add_fact_syms false) facts
     1.7 -          #> fold add_undefined_const (var_types ()))
     1.8 +          #> (case type_enc of
     1.9 +                Simple_Types _ => I
    1.10 +              | _ => fold add_undefined_const (var_types ())))
    1.11    end
    1.12  
    1.13  (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it