1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Tue Jun 26 11:14:40 2012 +0200
     1.3 @@ -2567,33 +2567,20 @@
     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 type_enc pred_sym s =
     1.8 +fun default_type pred_sym s =
     1.9    let
    1.10 -    val ind =
    1.11 -      case type_enc of
    1.12 -        Native _ =>
    1.13 -        (* ### FIXME: get rid of that, and move to "atp_problem.ML" *)
    1.14 -        if String.isPrefix type_const_prefix s orelse
    1.15 -           String.isPrefix tfree_prefix s then
    1.16 -          atype_of_types
    1.17 -        else
    1.18 -          individual_atype
    1.19 -      | _ => individual_atype
    1.20 -    fun typ 0 0 = if pred_sym then bool_atype else ind
    1.21 -      | typ 0 tm_ary = AFun (ind, typ 0 (tm_ary - 1))
    1.22 +    fun typ 0 0 = if pred_sym then bool_atype else individual_atype
    1.23 +      | typ 0 tm_ary = AFun (individual_atype, typ 0 (tm_ary - 1))
    1.24        | typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary)
    1.25    in typ end
    1.26  
    1.27  fun nary_type_constr_type n =
    1.28    funpow n (curry AFun atype_of_types) atype_of_types
    1.29  
    1.30 -fun undeclared_syms_in_problem type_enc problem =
    1.31 +fun undeclared_syms_in_problem problem =
    1.32    let
    1.33      fun do_sym (name as (s, _)) ty =
    1.34 -      if is_tptp_user_symbol s then
    1.35 -        Symtab.default (s, (name, ty))
    1.36 -      else
    1.37 -        I
    1.38 +      if is_tptp_user_symbol s then Symtab.default (s, (name, ty)) else I
    1.39      fun do_type (AType (name, tys)) =
    1.40          do_sym name (fn () => nary_type_constr_type (length tys))
    1.41          #> fold do_type tys
    1.42 @@ -2601,7 +2588,7 @@
    1.43        | do_type (APi (_, ty)) = do_type ty
    1.44      fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
    1.45          do_sym name
    1.46 -            (fn _ => default_type type_enc pred_sym s (length tys) (length tms))
    1.47 +            (fn _ => default_type pred_sym s (length tys) (length tms))
    1.48          #> fold do_type tys #> fold (do_term false) tms
    1.49        | do_term _ (AAbs (((_, ty), tm), args)) =
    1.50          do_type ty #> do_term false tm #> fold (do_term false) args
    1.51 @@ -2619,13 +2606,13 @@
    1.52      |> fold (fold do_problem_line o snd) problem
    1.53    end
    1.54  
    1.55 -fun declare_undeclared_syms_in_atp_problem type_enc problem =
    1.56 +fun declare_undeclared_syms_in_atp_problem problem =
    1.57    let
    1.58      val decls =
    1.59        Symtab.fold (fn (_, (("", ""), _)) => I (* already declared *)
    1.60                      | (s, (sym, ty)) =>
    1.61                        cons (Decl (type_decl_prefix ^ s, sym, ty ())))
    1.62 -                  (undeclared_syms_in_problem type_enc problem) []
    1.63 +                  (undeclared_syms_in_problem problem) []
    1.64    in (implicit_declsN, decls) :: problem end
    1.65  
    1.66  fun exists_subdtype P =
    1.67 @@ -2726,14 +2713,13 @@
    1.68         (free_typesN, formula_lines_for_free_types type_enc (facts @ conjs)),
    1.69         (conjsN, map (formula_line_for_conjecture ctxt mono type_enc) conjs)]
    1.70      val problem =
    1.71 -      problem
    1.72 -      |> (case format of
    1.73 -            CNF => ensure_cnf_problem
    1.74 -          | CNF_UEQ => filter_cnf_ueq_problem
    1.75 -          | FOF => I
    1.76 -          | TFF (_, TPTP_Implicit) => I
    1.77 -          | THF (_, TPTP_Implicit, _, _) => I
    1.78 -          | _ => declare_undeclared_syms_in_atp_problem type_enc)
    1.79 +      problem |> (case format of
    1.80 +                    CNF => ensure_cnf_problem
    1.81 +                  | CNF_UEQ => filter_cnf_ueq_problem
    1.82 +                  | FOF => I
    1.83 +                  | TFF (_, TPTP_Implicit) => I
    1.84 +                  | THF (_, TPTP_Implicit, _, _) => I
    1.85 +                  | _ => declare_undeclared_syms_in_atp_problem)
    1.86      val (problem, pool) = problem |> nice_atp_problem readable_names format
    1.87      fun add_sym_ary (s, {min_ary, ...} : sym_info) =
    1.88        min_ary > 0 ? Symtab.insert (op =) (s, min_ary)