--- a/src/Pure/Isar/calculation.ML Tue Apr 03 19:24:18 2007 +0200
+++ b/src/Pure/Isar/calculation.ML Tue Apr 03 19:24:19 2007 +0200
@@ -16,7 +16,8 @@
val symmetric: attribute
val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
- val finally: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
+ val finally_: (thmref * Attrib.src list) list option -> bool ->
+ Proof.state -> Proof.state Seq.seq
val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
val moreover: bool -> Proof.state -> Proof.state
val ultimately: bool -> Proof.state -> Proof.state
@@ -154,7 +155,7 @@
val also = calculate Proof.get_thmss false;
val also_i = calculate (K I) false;
-val finally = calculate Proof.get_thmss true;
+val finally_ = calculate Proof.get_thmss true;
val finally_i = calculate (K I) true;