# HG changeset patch
# User wenzelm
# Date 1030439040 -7200
# Node ID cafd1f98d65868c07e7eb1a6293cdfc532561aeb
# Parent  604d0f3622d63ee4306899c335d02c5ea8c3b786
dup_elim: improved error reporting;

diff -r 604d0f3622d6 -r cafd1f98d658 src/Provers/classical.ML
--- 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));