| changeset 17257 | 0ab67cb765da |
| parent 16976 | 377962871f5d |
| child 17271 | 2756a73f63a5 |
--- a/src/Provers/blast.ML Sat Sep 03 22:27:06 2005 +0200 +++ b/src/Provers/blast.ML Mon Sep 05 08:14:35 2005 +0200 @@ -455,7 +455,7 @@ (*Like dup_elim, but puts the duplicated major premise FIRST*) -fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd; +fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd; (*Rotate the assumptions in all new subgoals for the LIFO discipline*)