Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
revert guard logic -- make sure that typing information is generated for existentials
authorblanchet
Mon, 22 Aug 2011 15:02:45 +0200
changeset 44406 392c69bdb170
parent 44405 6fe1a89bb69a
child 44407 7b6629037127
revert guard logic -- make sure that typing information is generated for existentials
src/HOL/Tools/ATP/atp_translate.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle