# HG changeset patch
# User wenzelm
# Date 931635975 -7200
# Node ID a3c163ed1e04d0cc81787bf359f9d3454708b85d
# Parent  cfa87aef9ccdad81c1d50c3d9553c43f9613063e
dup_elim: use try to handle general exn;

diff -r cfa87aef9ccd -r a3c163ed1e04 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sat Jul 10 21:44:26 1999 +0200
+++ b/src/Provers/classical.ML	Sat Jul 10 21:46:15 1999 +0200
@@ -252,10 +252,12 @@
 (*Duplication of hazardous rules, for complete provers*)
 fun dup_intr th = zero_var_indexes (th RS classical);
 
-fun dup_elim th = 
-    th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd |> 
-    rule_by_tactic (TRYALL (etac revcut_rl))
-    handle _ => error ("Bad format for elimination rule\n" ^ string_of_thm th);
+fun dup_elim th =
+  (case try
+      (rule_by_tactic (TRYALL (etac revcut_rl)))
+      (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd) of
+    Some th' => th'
+  | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));
 
 
 (**** Classical rule sets ****)