src/Provers/classical.ML
changeset 17257 0ab67cb765da
parent 17084 fb0a80aef0be
child 17795 5b18c3343028
     1.1 --- a/src/Provers/classical.ML	Sat Sep 03 22:27:06 2005 +0200
     1.2 +++ b/src/Provers/classical.ML	Mon Sep 05 08:14:35 2005 +0200
     1.3 @@ -212,7 +212,7 @@
     1.4  fun dup_elim th =
     1.5    (case try (fn () =>
     1.6      rule_by_tactic (TRYALL (etac revcut_rl))
     1.7 -      (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of
     1.8 +      ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd)) () of
     1.9      SOME th' => th'
    1.10    | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th));
    1.11