# HG changeset patch
# User blanchet
# Date 1306249475 -7200
# Node ID 79c191d3ea031aebfcc968fbdb20f8e32b1e48c7
# Parent  b01cbbf0bcc594bbb9e99bc5c44503dc2a8f63c1
respect user's intention better when setting the CNF_UEQ type system (esp. w.r.t. "erased")

diff -r b01cbbf0bcc5 -r 79c191d3ea03 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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