# 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