src/Provers/classical.ML

 fun dup_intr th = zero_var_indexes (th RS classical);
 
 fun dup_elim th =
   (case try (fn () =>
     rule_by_tactic (TRYALL (etac revcut_rl))
-      (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of
+      ((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 ****)