src/HOL/Tools/SMT/smt_normalize.ML
changeset 41173 7c6178d45cc8
parent 41126 e0bd443c0fdd
child 41174 10eb369f8c01
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 16:29:56 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Dec 15 16:32:45 2010 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4        "must have the same kind: " ^ Syntax.string_of_term ctxt t)
     1.5  
     1.6    fun check_trigger_conv ctxt ct =
     1.7 -    if proper_quant false proper_trigger (Thm.term_of ct) then Conv.all_conv ct
     1.8 +    if proper_quant false proper_trigger (U.term_of ct) then Conv.all_conv ct
     1.9      else check_trigger_error ctxt (Thm.term_of ct)
    1.10  
    1.11  
    1.12 @@ -256,20 +256,20 @@
    1.13  
    1.14    fun is_weight (@{const SMT.weight} $ w $ t) =
    1.15          (case try HOLogic.dest_number w of
    1.16 -          SOME (_, i) => i > 0 andalso has_no_weight t
    1.17 +          SOME (_, i) => i >= 0 andalso has_no_weight t
    1.18          | _ => false)
    1.19      | is_weight t = has_no_weight t
    1.20  
    1.21    fun proper_trigger (@{const SMT.trigger} $ _ $ t) = is_weight t
    1.22 -    | proper_trigger t = has_no_weight t
    1.23 +    | proper_trigger t = is_weight t 
    1.24  
    1.25    fun check_weight_error ctxt t =
    1.26 -    error ("SMT weight must be a positive number and must only occur " ^
    1.27 +    error ("SMT weight must be a non-negative number and must only occur " ^
    1.28        "under the top-most quantifier and an optional trigger: " ^
    1.29        Syntax.string_of_term ctxt t)
    1.30  
    1.31    fun check_weight_conv ctxt ct =
    1.32 -    if U.under_quant proper_trigger (Thm.term_of ct) then Conv.all_conv ct
    1.33 +    if U.under_quant proper_trigger (U.term_of ct) then Conv.all_conv ct
    1.34      else check_weight_error ctxt (Thm.term_of ct)
    1.35  
    1.36