# HG changeset patch
# User blanchet
# Date 1292419744 -3600
# Node ID ceb81a08534e1f1afd256870c15ec3ae42d2fe7c
# Parent  2181c47a02fe2523c36345c4234058a5c49162a6
workaround for bug in weight handling -- sometimes numerals got replaced by Vars and this confused the weight extractor

diff -r 2181c47a02fe -r ceb81a08534e src/HOL/Tools/SMT/smt_translate.ML
--- 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)