# HG changeset patch # User blanchet # Date 1314018165 -7200 # Node ID 392c69bdb1701eb2552ff9898cf2bd012af8035e # Parent 6fe1a89bb69a9f35acb9422b5e167c4ff5b00088 revert guard logic -- make sure that typing information is generated for existentials diff -r 6fe1a89bb69a -r 392c69bdb170 src/HOL/Tools/ATP/atp_translate.ML --- a/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 +++ b/src/HOL/Tools/ATP/atp_translate.ML Mon Aug 22 15:02:45 2011 +0200 @@ -1598,9 +1598,9 @@ accum orelse (is_tptp_equal s andalso member (op =) tms (ATerm (name, []))) | is_var_positively_naked_in_term _ _ _ _ = true -fun should_guard_var_in_formula _ _ (SOME false) _ = false - | should_guard_var_in_formula pos phi _ name = +fun should_guard_var_in_formula pos phi (SOME true) name = formula_fold pos (is_var_positively_naked_in_term name) phi false + | should_guard_var_in_formula _ _ _ _ = true fun should_generate_tag_bound_decl _ _ _ (SOME true) _ = false | should_generate_tag_bound_decl ctxt mono (Tags (_, level, Nonuniform)) _ T =