# HG changeset patch
# User wenzelm
# Date 1005844532 -3600
# Node ID 571d9c28864025b154b1b94d34d85a9c5f2fbbad
# Parent  af10de5ec7cc90c7c8d73c0f58bffba137bde074
avoid handle _;

diff -r af10de5ec7cc -r 571d9c288640 src/ZF/Datatype.ML
--- a/src/ZF/Datatype.ML	Thu Nov 15 18:15:13 2001 +0100
+++ b/src/ZF/Datatype.ML	Thu Nov 15 18:15:32 2001 +0100
@@ -71,10 +71,12 @@
        val (lhs,rhs) = FOLogic.dest_eq old
        val (lhead, largs) = strip_comb lhs
        and (rhead, rargs) = strip_comb rhs
-       val lname = #1 (dest_Const lhead)
-       and rname = #1 (dest_Const rhead)
+       val lname = #1 (dest_Const lhead) handle TERM _ => raise Match;
+       val rname = #1 (dest_Const rhead) handle TERM _ => raise Match;
        val lcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, lname))
-       and rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname))
+         handle Library.OPTION => raise Match;
+       val rcon_info = the (Symtab.lookup (ConstructorsData.get_sg sg, rname))
+         handle Library.OPTION => raise Match;
        val new = 
            if #big_rec_name lcon_info = #big_rec_name rcon_info 
                andalso not (null (#free_iffs lcon_info)) then
@@ -87,10 +89,11 @@
        val goal = Logic.mk_equals (old, new)
        val thm = Tactic.prove sg [] [] goal (fn _ => rtac iff_reflection 1 THEN
            simp_tac (datatype_ss addsimps #free_iffs lcon_info) 1)
-         handle ERROR =>
-         error ("data_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal)
+         handle ERROR_MESSAGE msg =>
+         (warning (msg ^ "\ndata_free simproc:\nfailed to prove " ^ Sign.string_of_term sg goal);
+          raise Match)
    in Some thm end
-   handle _ => None;
+   handle Match => None;
 
 
  val conv = 
diff -r af10de5ec7cc -r 571d9c288640 src/ZF/Tools/primrec_package.ML
--- a/src/ZF/Tools/primrec_package.ML	Thu Nov 15 18:15:13 2001 +0100
+++ b/src/ZF/Tools/primrec_package.ML	Thu Nov 15 18:15:32 2001 +0100
@@ -41,11 +41,11 @@
   let
     val (lhs, rhs) =
         if null (term_vars eq) then
-            dest_eqn eq handle _ => raise RecError "not a proper equation"
+            dest_eqn eq handle TERM _ => raise RecError "not a proper equation"
         else raise RecError "illegal schematic variable(s)";
 
     val (recfun, args) = strip_comb lhs;
-    val (fname, ftype) = dest_Const recfun handle _ =>
+    val (fname, ftype) = dest_Const recfun handle TERM _ =>
       raise RecError "function is not declared as constant in theory";
 
     val (ls_frees, rest)  = take_prefix is_Free args;
@@ -55,15 +55,15 @@
       if null middle then raise RecError "constructor missing"
       else strip_comb (hd middle);
     val (cname, _) = dest_Const constr
-      handle _ => raise RecError "ill-formed constructor";
+      handle TERM _ => raise RecError "ill-formed constructor";
     val con_info = the (Symtab.lookup (ConstructorsData.get thy, cname))
-      handle _ =>
+      handle Library.OPTION =>
       raise RecError "cannot determine datatype associated with function"
 
     val (ls, cargs, rs) = (map dest_Free ls_frees,
                            map dest_Free cargs_frees,
                            map dest_Free rs_frees)
-      handle _ => raise RecError "illegal argument in pattern";
+      handle TERM _ => raise RecError "illegal argument in pattern";
     val lfrees = ls @ rs @ cargs;
 
     (*Constructor, frees to left of pattern, pattern variables,