# 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 =