src/HOL/Tools/SMT/smt_real.ML
changeset 41281 679118e35378
parent 41280 a7de9d36f4f2
child 41302 0485186839a7
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 17:55:56 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Sun Dec 19 18:54:29 2010 +0100
     1.3 @@ -35,11 +35,15 @@
     1.4      | is_linear [t, u] = U.is_number t orelse U.is_number u
     1.5      | is_linear _ = false
     1.6  
     1.7 -  fun times _ T ts = if is_linear ts then SOME ((("*", 2), T), ts, T) else NONE
     1.8 +  fun mk_times ts = Term.list_comb (@{const times (real)}, ts)
     1.9 +
    1.10 +  fun times _ T ts = if is_linear ts then SOME ("*", 2, ts, mk_times) else NONE
    1.11      | times _ _ _  = NONE
    1.12  
    1.13 +  fun mk_divide ts = Term.list_comb (@{const divide (real)}, ts)
    1.14 +
    1.15    fun divide _ T (ts as [_, t]) =
    1.16 -        if U.is_number t then SOME ((("/", 2), T), ts, T) else NONE
    1.17 +        if U.is_number t then SOME ("/", 2, ts, mk_divide) else NONE
    1.18      | divide _ _ _ = NONE
    1.19  in
    1.20