1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Mon Aug 22 15:02:45 2011 +0200
     1.3 @@ -1598,9 +1598,9 @@
     1.4      accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, [])))
     1.5    | is_var_positively_naked_in_term _ _ _ _ = true
     1.6  
     1.7 -fun should_guard_var_in_formula _ _ (SOME false) _ = false
     1.8 -  | should_guard_var_in_formula pos phi _ name =
     1.9 +fun should_guard_var_in_formula pos phi (SOME true) name =
    1.10      formula_fold pos (is_var_positively_naked_in_term name) phi false
    1.11 +  | should_guard_var_in_formula _ _ _ _ = true
    1.12  
    1.13  fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false
    1.14    | should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =