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
```