workaround for bug in weight handling -- sometimes numerals got replaced by Vars and this confused the weight extractor

--- a/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 13:35:50 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_translate.ML	Wed Dec 15 14:29:04 2010 +0100
@@ -496,7 +496,14 @@
   | group_quant _ Ts t = (Ts, t)
 
 fun dest_weight (@{const SMT.weight} $ w $ t) =
-      (SOME (snd (HOLogic.dest_number w)), t)
+      ((SOME (snd (HOLogic.dest_number w)), t)
+       handle TERM _ =>
+                (case w of
+                  Var ((s, _), _) => (* FIXME: temporary workaround *)
+                    (case Int.fromString s of
+                      SOME n => (SOME n, t)
+                    | NONE => raise TERM ("bad weight", [w]))
+                 | _ => raise TERM ("bad weight", [w])))
   | dest_weight t = (NONE, t)
 
 fun dest_pat (Const (@{const_name pat}, _) $ t) = (t, true)