dup_elim: improved error reporting;

--- a/src/Provers/classical.ML	Tue Aug 27 11:03:05 2002 +0200
+++ b/src/Provers/classical.ML	Tue Aug 27 11:04:00 2002 +0200
@@ -205,9 +205,9 @@
 fun dup_intr th = zero_var_indexes (th RS classical);
 
 fun dup_elim th =
-  (case try
-      (rule_by_tactic (TRYALL (etac revcut_rl)))
-      (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd) of
+  (case try (fn () =>
+    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));