1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 10:16:14 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 05 10:24:12 2011 +0200
     1.3 @@ -887,7 +887,7 @@
     1.4        case type_sys of
     1.5          Preds (Polymorphic, All_Types) => insert_type #3 decl decls
     1.6        | _ => insert (op =) decl decls
     1.7 -    fun do_term tm =
     1.8 +    and do_term tm =
     1.9        let val (head, args) = strip_combterm_comb tm in
    1.10          (case head of
    1.11             CombConst ((s, s'), T, T_args) =>