1.1 --- a/src/HOL/Tools/ATP/atp_problem.ML	Wed Jul 06 17:19:34 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem.ML	Wed Jul 06 17:19:34 2011 +0100
     1.3 @@ -273,8 +273,10 @@
     1.4      |> enclose "(" ")"
     1.5    | string_for_formula format (AAtom tm) = string_for_term format tm
     1.6  
     1.7 -val default_source =
     1.8 -  ATerm ("inference", ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
     1.9 +fun the_source (SOME source) = source
    1.10 +  | the_source NONE =
    1.11 +    ATerm ("inference",
    1.12 +           ATerm ("isabelle", []) :: replicate 2 (ATerm ("[]", [])))
    1.13  
    1.14  fun string_for_format CNF = tptp_cnf
    1.15    | string_for_format CNF_UEQ = tptp_cnf
    1.16 @@ -292,7 +294,7 @@
    1.17         (NONE, NONE) => ""
    1.18       | (SOME tm, NONE) => ", " ^ string_for_term format tm
    1.19       | (_, SOME tm) =>
    1.20 -       ", " ^ string_for_term format (source |> the_default default_source) ^
    1.21 +       ", " ^ string_for_term format (the_source source) ^
    1.22         ", " ^ string_for_term format tm) ^ ").\n"
    1.23  fun tptp_lines_for_atp_problem format problem =
    1.24    "% This file was generated by Isabelle (most likely Sledgehammer)\n\

     2.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 06 17:19:34 2011 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Wed Jul 06 17:19:34 2011 +0100
     2.3 @@ -752,7 +752,7 @@
     2.4    | generic_mangled_type_name f (ATerm (name, tys)) =
     2.5      f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
     2.6      ^ ")"
     2.7 -  | generic_mangled_type_name f _ = raise Fail "unexpected type abstraction"
     2.8 +  | generic_mangled_type_name _ _ = raise Fail "unexpected type abstraction"
     2.9  
    2.10  val bool_atype = AType (`I tptp_bool_type)
    2.11  
    2.12 @@ -771,7 +771,7 @@
    2.13      fun to_afun f1 f2 tys = AFun (f1 (hd tys), f2 (nth tys 1))
    2.14      fun to_fo 0 ty = if pred_sym then bool_atype else to_atype ty
    2.15        | to_fo ary (ATerm (_, tys)) = to_afun to_atype (to_fo (ary - 1)) tys
    2.16 -      | to_fo ary _ = raise Fail "unexpected type abstraction"
    2.17 +      | to_fo _ _ = raise Fail "unexpected type abstraction"
    2.18      fun to_ho (ty as ATerm ((s, _), tys)) =
    2.19          if s = tptp_fun_type then to_afun to_ho to_ho tys else to_atype ty
    2.20        | to_ho _ = raise Fail "unexpected type abstraction"
    2.21 @@ -1477,7 +1477,7 @@
    2.22  fun is_var_positively_naked_in_term _ (SOME false) _ accum = accum
    2.23    | is_var_positively_naked_in_term name _ (ATerm ((s, _), tms)) accum =
    2.24      accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
    2.25 -  | is_var_positively_naked_in_term name _ _ _ = true
    2.26 +  | is_var_positively_naked_in_term _ _ _ _ = true
    2.27  fun should_predicate_on_var_in_formula pos phi (SOME true) name =
    2.28      formula_fold pos (is_var_positively_naked_in_term name) phi false
    2.29    | should_predicate_on_var_in_formula _ _ _ _ = true
    2.30 @@ -1489,7 +1489,8 @@
    2.31    CombConst (type_tag, T --> T, [T])
    2.32    |> enforce_type_arg_policy_in_combterm ctxt format type_enc
    2.33    |> ho_term_from_combterm ctxt format nonmono_Ts type_enc (Top_Level pos)
    2.34 -  |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm]))
    2.35 +  |> (fn ATerm (s, tms) => ATerm (s, tms @ [tm])
    2.36 +       | _ => raise Fail "unexpected lambda-abstraction")
    2.37  and ho_term_from_combterm ctxt format nonmono_Ts type_enc =
    2.38    let
    2.39      fun aux site u =