src/HOL/Tools/SMT/smt_translate.ML
changeset 41165 ceb81a08534e
parent 41127 2ea84c8535c6
child 41172 a17c2d669c40
child 41193 dc33b8ea4526
     1.1 --- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 13:35:50 2010 +0100
     1.2 +++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 14:29:04 2010 +0100
     1.3 @@ -496,7 +496,14 @@
     1.4    | group_quant _ Ts t = (Ts, t)
     1.5  
     1.6  fun dest_weight (@{const SMT.weight} $ w $ t) =
     1.7 -      (SOME (snd (HOLogic.dest_number w)), t)
     1.8 +      ((SOME (snd (HOLogic.dest_number w)), t)
     1.9 +       handle TERM _ =>
    1.10 +                (case w of
    1.11 +                  Var ((s, _), _) => (* FIXME: temporary workaround *)
    1.12 +                    (case Int.fromString s of
    1.13 +                      SOME n => (SOME n, t)
    1.14 +                    | NONE => raise TERM ("bad weight", [w]))
    1.15 +                 | _ => raise TERM ("bad weight", [w])))
    1.16    | dest_weight t = (NONE, t)
    1.17  
    1.18  fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)