1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Jul 25 14:10:12 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Jul 25 14:10:12 2011 +0200
     1.3 @@ -1155,9 +1155,14 @@
     1.4    fact_lift (formula_fold NONE
     1.5                            (K (add_iterm_syms_to_table ctxt explicit_apply)))
     1.6  
     1.7 +val undefined_name = make_fixed_const @{const_name undefined}
     1.8 +val tvar_a = TVar (("'a", 0), HOLogic.typeS)
     1.9 +
    1.10  val default_sym_tab_entries : (string * sym_info) list =
    1.11    (prefixed_predicator_name,
    1.12     {pred_sym = true, min_ary = 1, max_ary = 1, types = []}) ::
    1.13 +  (undefined_name,
    1.14 +   {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
    1.15    ([tptp_false, tptp_true]
    1.16     |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
    1.17    ([tptp_equal, tptp_old_equal]
    1.18 @@ -1650,7 +1655,7 @@
    1.19  
    1.20  fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
    1.21    let
    1.22 -    fun add_iterm in_conj tm =
    1.23 +    fun add_iterm_syms in_conj tm =
    1.24        let val (head, args) = strip_iterm_comb tm in
    1.25          (case head of
    1.26             IConst ((s, s'), T, T_args) =>
    1.27 @@ -1662,15 +1667,31 @@
    1.28               else
    1.29                 I
    1.30             end
    1.31 -         | IAbs (_, tm) => add_iterm in_conj tm
    1.32 +         | IAbs (_, tm) => add_iterm_syms in_conj tm
    1.33           | _ => I)
    1.34 -        #> fold (add_iterm in_conj) args
    1.35 +        #> fold (add_iterm_syms in_conj) args
    1.36        end
    1.37 -    fun add_fact in_conj = fact_lift (formula_fold NONE (K (add_iterm in_conj)))
    1.38 +    fun add_fact_syms in_conj =
    1.39 +      fact_lift (formula_fold NONE (K (add_iterm_syms in_conj)))
    1.40 +    fun add_formula_var_types (AQuant (_, xs, phi)) =
    1.41 +        fold (fn (_, SOME T) => insert_type ctxt I T | _ => I) xs
    1.42 +        #> add_formula_var_types phi
    1.43 +      | add_formula_var_types (AConn (_, phis)) =
    1.44 +        fold add_formula_var_types phis
    1.45 +      | add_formula_var_types _ = I
    1.46 +    fun var_types () =
    1.47 +      if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
    1.48 +      else fold (fact_lift add_formula_var_types) (conjs @ facts) []
    1.49 +    fun add_undefined_const T =
    1.50 +      Symtab.map_default (undefined_name, [])
    1.51 +          (insert_type ctxt #3 (@{const_name undefined}, [T], T, false, 0,
    1.52 +                                false))
    1.53    in
    1.54      Symtab.empty
    1.55      |> is_type_enc_fairly_sound type_enc
    1.56 -       ? (fold (add_fact true) conjs #> fold (add_fact false) facts)
    1.57 +       ? (fold (add_fact_syms true) conjs
    1.58 +          #> fold (add_fact_syms false) facts
    1.59 +          #> fold add_undefined_const (var_types ()))
    1.60    end
    1.61  
    1.62  (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it
    1.63 @@ -1897,7 +1918,7 @@
    1.64           polymorphism_of_type_enc type_enc <> Polymorphic then
    1.65          nonmono_Ts
    1.66        else
    1.67 -        [TVar (("'a", 0), HOLogic.typeS)]
    1.68 +        [tvar_a]
    1.69      val sym_decl_lines =
    1.70        (conjs, helpers @ facts)
    1.71        |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab