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.
respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")
authorblanchet
Tue, 24 May 2011 17:04:35 +0200
changeset 42972 79c191d3ea03
parent 42971 b01cbbf0bcc5
child 42973 6b39a2098ffd
respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")
src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 13:29:32 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue May 24 17:04:35 2011 +0200
@@ -450,9 +450,10 @@
       (FOF, type_sys)
     else if member (op =) formats CNF_UEQ then
       (CNF_UEQ, case type_sys of
-                  Tags _ => type_sys
-                | _ => Preds (polymorphism_of_type_sys type_sys,
-                              Const_Arg_Types, Light))
+                  Preds stuff =>
+                  (if is_type_sys_fairly_sound type_sys then Preds else Tags)
+                      stuff
+                | _ => type_sys)
     else
       (* We could return "type_sys" unchanged for TFF but this would require the
          TFF provers to accept problems in which constants are implicitly
isabelle