# HG changeset patch
# User paulson
# Date 956911443 -7200
# Node ID ebb07113c4f79e36d0c9ca3f3b1201b8c418e175
# Parent  026f37a86ea7dd655c0bc89f8ae1af0465459084
inserted triviality check

diff -r 026f37a86ea7 -r ebb07113c4f7 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Tue Apr 25 08:09:10 2000 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Fri Apr 28 10:44:03 2000 +0200
@@ -81,10 +81,13 @@
       fun newshape (i,terms) = Data.mk_sum (Data.mk_coeff(i,u)::terms)
       val reshapes =  (*Move i*u to the front and put j*u into standard form
 		      i + #m + j + k == #m + i + (j + k) *)
-	    listof (Data.prove_conv [Data.norm_tac] sg 
-		    (t, 
-		     Data.mk_bal (newshape(n1,terms1'), 
-				  newshape(n2,terms2'))))
+	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
+		raise TERM("cancel_numerals", []) 
+	    else
+		listof (Data.prove_conv [Data.norm_tac] sg 
+			(t, 
+			 Data.mk_bal (newshape(n1,terms1'), 
+				      newshape(n2,terms2'))))
   in
 
       if n2<=n1 then