dup_elim: improved error reporting;
authorwenzelm
Tue Aug 27 11:04:00 2002 +0200 (2002-08-27 ago)
changeset 13525cafd1f98d658
parent 13524 604d0f3622d6
child 13526 9269275e5da6
dup_elim: improved error reporting;
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Tue Aug 27 11:03:05 2002 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Aug 27 11:04:00 2002 +0200
     1.3 @@ -205,9 +205,9 @@
     1.4  fun dup_intr th = zero_var_indexes (th RS classical);
     1.5  
     1.6  fun dup_elim th =
     1.7 -  (case try
     1.8 -      (rule_by_tactic (TRYALL (etac revcut_rl)))
     1.9 -      (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd) of
    1.10 +  (case try (fn () =>
    1.11 +    rule_by_tactic (TRYALL (etac revcut_rl))
    1.12 +      (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of
    1.13      Some th' => th'
    1.14    | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));
    1.15