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 @@ -1155,13 +1155,12 @@
     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 +  (make_fixed_const @{const_name undefined},
    1.15     {pred_sym = false, min_ary = 0, max_ary = 0, types = []}) ::
    1.16    ([tptp_false, tptp_true]
    1.17     |> map (rpair {pred_sym = true, min_ary = 0, max_ary = 0, types = []})) @
    1.18 @@ -1653,7 +1652,8 @@
    1.19     | Tags (_, _, Lightweight) => true
    1.20     | _ => not pred_sym)
    1.21  
    1.22 -fun sym_decl_table_for_facts ctxt type_enc repaired_sym_tab (conjs, facts) =
    1.23 +fun sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
    1.24 +                             (conjs, facts) =
    1.25    let
    1.26      fun add_iterm_syms in_conj tm =
    1.27        let val (head, args) = strip_iterm_comb tm in
    1.28 @@ -1683,9 +1683,14 @@
    1.29        if polymorphism_of_type_enc type_enc = Polymorphic then [tvar_a]
    1.30        else fold (fact_lift add_formula_var_types) (conjs @ facts) []
    1.31      fun add_undefined_const T =
    1.32 -      Symtab.map_default (undefined_name, [])
    1.33 -          (insert_type ctxt #3 (@{const_name undefined}, [T], T, false, 0,
    1.34 -                                false))
    1.35 +      let
    1.36 +        val (s, s') =
    1.37 +          `make_fixed_const @{const_name undefined}
    1.38 +          |> mangled_const_name format type_enc [T]
    1.39 +      in
    1.40 +        Symtab.map_default (s, [])
    1.41 +                           (insert_type ctxt #3 (s', [T], T, false, 0, false))
    1.42 +      end
    1.43    in
    1.44      Symtab.empty
    1.45      |> is_type_enc_fairly_sound type_enc
    1.46 @@ -1921,7 +1926,7 @@
    1.47          [tvar_a]
    1.48      val sym_decl_lines =
    1.49        (conjs, helpers @ facts)
    1.50 -      |> sym_decl_table_for_facts ctxt type_enc repaired_sym_tab
    1.51 +      |> sym_decl_table_for_facts ctxt format type_enc repaired_sym_tab
    1.52        |> problem_lines_for_sym_decl_table ctxt format conj_sym_kind nonmono_Ts
    1.53                                                 poly_nonmono_Ts type_enc
    1.54      val helper_lines =