1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Dec 14 17:49:42 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Dec 14 18:07:32 2011 +0100
     1.3 @@ -2338,11 +2338,14 @@
     1.4     symbols (with "$i" as the type of individuals), but some provers (e.g.,
     1.5     SNARK) require explicit declarations. The situation is similar for THF. *)
     1.6  
     1.7 -fun default_type pred_sym s =
     1.8 +fun default_type type_enc pred_sym s =
     1.9    let
    1.10      val ind =
    1.11 -      if String.isPrefix type_const_prefix s then atype_of_types
    1.12 -      else individual_atype
    1.13 +      case type_enc of
    1.14 +        Simple_Types _ =>
    1.15 +        if String.isPrefix type_const_prefix s then atype_of_types
    1.16 +        else individual_atype
    1.17 +      | _ => individual_atype
    1.18      fun typ 0 = if pred_sym then bool_atype else ind
    1.19        | typ ary = AFun (ind, typ (ary - 1))
    1.20    in typ end
    1.21 @@ -2350,7 +2353,7 @@
    1.22  fun nary_type_constr_type n =
    1.23    funpow n (curry AFun atype_of_types) atype_of_types
    1.24  
    1.25 -fun undeclared_syms_in_problem problem =
    1.26 +fun undeclared_syms_in_problem type_enc problem =
    1.27    let
    1.28      val declared = declared_syms_in_problem problem
    1.29      fun do_sym name ty =
    1.30 @@ -2363,7 +2366,7 @@
    1.31        | do_type (ATyAbs (_, ty)) = do_type ty
    1.32      fun do_term pred_sym (ATerm (name as (s, _), tms)) =
    1.33          is_tptp_user_symbol s
    1.34 -        ? do_sym name (fn _ => default_type pred_sym s (length tms))
    1.35 +        ? do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
    1.36          #> fold (do_term false) tms
    1.37        | do_term _ (AAbs ((_, ty), tm)) = do_type ty #> do_term false tm
    1.38      fun do_formula (AQuant (_, xs, phi)) =
    1.39 @@ -2377,11 +2380,11 @@
    1.40      |> filter_out (is_built_in_tptp_symbol o fst o fst)
    1.41    end
    1.42  
    1.43 -fun declare_undeclared_syms_in_atp_problem problem =
    1.44 +fun declare_undeclared_syms_in_atp_problem type_enc problem =
    1.45    let
    1.46      val decls =
    1.47        problem
    1.48 -      |> undeclared_syms_in_problem
    1.49 +      |> undeclared_syms_in_problem type_enc
    1.50        |> sort_wrt (fst o fst)
    1.51        |> map (fn (x as (s, _), ty) => Decl (type_decl_prefix ^ s, x, ty ()))
    1.52    in (implicit_declsN, decls) :: problem end
    1.53 @@ -2464,7 +2467,7 @@
    1.54            | FOF => I
    1.55            | TFF (_, TPTP_Implicit) => I
    1.56            | THF (_, TPTP_Implicit, _) => I
    1.57 -          | _ => declare_undeclared_syms_in_atp_problem)
    1.58 +          | _ => declare_undeclared_syms_in_atp_problem type_enc)
    1.59      val (problem, pool) = problem |> nice_atp_problem readable_names
    1.60      fun add_sym_ary (s, {min_ary, ...} : sym_info) =
    1.61        min_ary > 0 ? Symtab.insert (op =) (s, min_ary)