src/HOL/Tools/SMT/smt_translate.ML
changeset 41173 7c6178d45cc8
parent 41172 a17c2d669c40
child 41194 9796e5e01b61
child 41195 f59491d56327
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 16:29:56 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 16:32:45 2010 +0100
     1.3 @@ -147,6 +147,8 @@
     1.4      fun mark t =
     1.5        (case Term.strip_comb t of
     1.6          (u as Const (@{const_name If}, _), ts) => marks u ts
     1.7 +      | (u as @{const SMT.weight}, [t1, t2]) =>
     1.8 +          mark t2 #>> (fn t2' => u $ t1 $ t2')
     1.9        | (u as Const c, ts) =>
    1.10            (case B.builtin_num ctxt t of
    1.11              SOME (n, T) =>
    1.12 @@ -494,14 +496,7 @@
    1.13    | group_quant _ Ts t = (Ts, t)
    1.14  
    1.15  fun dest_weight (@{const SMT.weight} $ w $ t) =
    1.16 -      ((SOME (snd (HOLogic.dest_number w)), t)
    1.17 -       handle TERM _ =>
    1.18 -                (case w of
    1.19 -                  Var ((s, _), _) => (* FIXME: temporary workaround *)
    1.20 -                    (case Int.fromString s of
    1.21 -                      SOME n => (SOME n, t)
    1.22 -                    | NONE => raise TERM ("bad weight", [w]))
    1.23 -                 | _ => raise TERM ("bad weight", [w])))
    1.24 +      (SOME (snd (HOLogic.dest_number w)), t)
    1.25    | dest_weight t = (NONE, t)
    1.26  
    1.27  fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)