--- a/src/Provers/Arith/fast_lin_arith.ML Mon Jun 08 22:29:37 2009 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Jun 09 09:22:58 2009 +0200
@@ -163,7 +163,6 @@
| NotLeD of injust
| NotLeDD of injust
| Multiplied of int * injust
- | Multiplied2 of int * injust
| Added of injust * injust;
datatype lineq = Lineq of int * lineq_type * int list * injust;
@@ -523,7 +522,6 @@
| mk (NotLessD j) = trace_thm "NL" (mk j RS LA_Logic.not_lessD)
| mk (Added (j1, j2)) = simp (trace_thm "+" (add_thms (mk j1) (mk j2)))
| mk (Multiplied (n, j)) = (trace_msg ("*" ^ string_of_int n); trace_thm "*" (mult_thm (n, mk j)))
- | mk (Multiplied2 (n, j)) = (trace_msg ("**" ^ string_of_int n); trace_thm "**" (mult_thm (n, mk j)))
in
let
@@ -570,7 +568,7 @@
val diff = map2 (curry (op -)) rhsa lhsa
val c = i-j
val just = Asm k
- fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied2(m,j))
+ fun lineq(c,le,cs,j) = Lineq(c,le,cs, if m=1 then j else Multiplied(m,j))
in case rel of
"<=" => lineq(c,Le,diff,just)
| "~<=" => if discrete