# HG changeset patch
# User boehmes
# Date 1244532178 -7200
# Node ID dd989ea86cf076dbb15a1a56f267f57fcb5bce56
# Parent  e0f2bb4b002167070c1fe1443fe35f4a380abc13
tuned

diff -r e0f2bb4b0021 -r dd989ea86cf0 src/Provers/Arith/fast_lin_arith.ML
--- 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