# HG changeset patch
# User wenzelm
# Date 1005844697 -3600
# Node ID 60d52181840cb2596ebc9e77bacbb98ea4587630
# Parent  f3545bd6669bfbbba6f717d12e320112c77263f9
no handle ERROR;

diff -r f3545bd6669b -r 60d52181840c src/ZF/arith_data.ML
--- a/src/ZF/arith_data.ML	Thu Nov 15 18:16:17 2001 +0100
+++ b/src/ZF/arith_data.ML	Thu Nov 15 18:18:17 2001 +0100
@@ -75,8 +75,8 @@
       val goal = Logic.list_implies (map (#prop o Thm.rep_thm) hyps',
         FOLogic.mk_Trueprop (mk_eq_iff (t, u)));
   in Some (hyps' MRS Tactic.prove sg [] [] goal (K (EVERY tacs)))
-      handle ERROR => 
-	(warning ("Cancellation failed: no typing information? (" ^ name ^ ")"); None)
+      handle ERROR_MESSAGE msg => 
+	(warning (msg ^ "\nCancellation failed: no typing information? (" ^ name ^ ")"); None)
   end;
 
 fun prep_simproc (name, pats, proc) = Simplifier.mk_simproc name pats proc;