# HG changeset patch
# User paulson
# Date 956309498 -7200
# Node ID 8043130d3dcf11bd28e76ee87b50fe0107c6fbb3
# Parent  9139453d70332ee1a0d05fb306bf5ca28a2d633e
cleaner exceptions

diff -r 9139453d7033 -r 8043130d3dcf src/Provers/Arith/fold_Suc.ML
--- a/src/Provers/Arith/fold_Suc.ML	Fri Apr 21 11:31:03 2000 +0200
+++ b/src/Provers/Arith/fold_Suc.ML	Fri Apr 21 11:31:38 2000 +0200
@@ -29,20 +29,22 @@
 =
 struct
 
+fun listof None = []
+  | listof (Some x) = [x];
+
 fun proc sg _ t =
   let val sum = Data.dest_Suc t 
       val terms = Data.dest_sum sum
       val (m, lit_m, terms') = Data.find_first_numeral terms
       val assocs =  (*If needed, rewrite the literal m to the front:
 		     i + #m + j + k == #m + i + (j + k) *)
-	  [the (Data.prove_conv [Data.add_norm_tac] sg
-		(sum, Data.mk_sum (lit_m::terms')))]
-	  handle _ => []
+	  listof (Data.prove_conv [Data.add_norm_tac] sg
+		  (sum, Data.mk_sum (lit_m::terms')))
   in
       Data.prove_conv 
         [Data.numeral_simp_tac assocs] sg
 	(t, Data.mk_sum (Data.mk_numeral (m+1) :: terms'))
   end
-  handle _ => None;
+  handle TERM _ => None;
 
 end;