# HG changeset patch
# User paulson
# Date 957286478 -7200
# Node ID 2d4afbc468010b7b35f5fb7869625fb8444939cf
# Parent  268195e8c0173160caeff98d8f7b33af9e985c71
various bug fixes

diff -r 268195e8c017 -r 2d4afbc46801 src/Provers/Arith/cancel_numerals.ML
--- a/src/Provers/Arith/cancel_numerals.ML	Tue May 02 18:45:17 2000 +0200
+++ b/src/Provers/Arith/cancel_numerals.ML	Tue May 02 18:54:38 2000 +0200
@@ -37,6 +37,7 @@
   val bal_add2: thm
   (*proof tools*)
   val prove_conv: tactic list -> Sign.sg -> term * term -> thm option
+  val subst_tac: thm option -> tactic
   val norm_tac: tactic
   val numeral_simp_tac: tactic
 end;
@@ -49,13 +50,9 @@
 =
 struct
 
-fun listof None = []
-  | listof (Some x) = [x];
-
-(*If t = #n*u then put u in the table*)
+(*For t = #n*u then put u in the table*)
 fun update_by_coeff (tab, t) =
-  Termtab.update ((#2 (Data.dest_coeff t), ()), tab)
-  handle TERM _ => tab;
+  Termtab.update ((#2 (Data.dest_coeff t), ()), tab);
 
 (*a left-to-right scan of terms1, seeking a term of the form #n*u, where
   #m*u is in terms2 for some m*)
@@ -67,7 +64,6 @@
 	      in  if is_some (Termtab.lookup (tab2, u)) then u
 		  else seek terms
 	      end
-	      handle TERM _ => seek terms
   in  seek terms1 end;
 
 (*the simplification procedure*)
@@ -79,28 +75,29 @@
       val (n1, terms1') = Data.find_first_coeff u terms1
       and (n2, terms2') = Data.find_first_coeff u terms2
       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) *)
+      val reshape =  (*Move i*u to the front and put j*u into standard form
+		       i + #m + j + k == #m + i + (j + k) *)
 	    if n1=0 orelse n2=0 then   (*trivial, so do nothing*)
 		raise TERM("cancel_numerals", []) 
-	    else
-		listof (Data.prove_conv [Data.norm_tac] sg 
+	    else Data.prove_conv [Data.norm_tac] sg 
 			(t, 
 			 Data.mk_bal (newshape(n1,terms1'), 
-				      newshape(n2,terms2'))))
+				      newshape(n2,terms2')))
   in
 
       if n2<=n1 then 
 	  Data.prove_conv 
-	     [rewrite_goals_tac reshapes, rtac Data.bal_add1 1,
+	     [Data.subst_tac reshape, rtac Data.bal_add1 1,
 	      Data.numeral_simp_tac] sg
 	     (t, Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum terms2'))
       else
 	  Data.prove_conv 
-	     [rewrite_goals_tac reshapes, rtac Data.bal_add2 1,
+	     [Data.subst_tac reshape, rtac Data.bal_add2 1,
 	      Data.numeral_simp_tac] sg
 	     (t, Data.mk_bal (Data.mk_sum terms1', newshape(n2-n1,terms2')))
   end
-  handle TERM _ => None;
+  handle TERM _ => None
+       | TYPE _ => None;   (*Typically (if thy doesn't include Numeral)
+			     Undeclared type constructor "Numeral.bin"*)
 
 end;