1.1 --- a/src/Pure/Isar/calculation.ML	Wed Mar 19 18:15:25 2008 +0100
     1.2 +++ b/src/Pure/Isar/calculation.ML	Wed Mar 19 22:27:57 2008 +0100
     1.3 @@ -14,9 +14,9 @@
     1.4    val sym_add: attribute
     1.5    val sym_del: attribute
     1.6    val symmetric: attribute
     1.7 -  val also: (thmref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
     1.8 +  val also: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq
     1.9    val also_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.10 -  val finally_: (thmref * Attrib.src list) list option -> bool ->
    1.11 +  val finally_: (Facts.ref * Attrib.src list) list option -> bool ->
    1.12      Proof.state -> Proof.state Seq.seq
    1.13    val finally_i: thm list option -> bool -> Proof.state -> Proof.state Seq.seq
    1.14    val moreover: bool -> Proof.state -> Proof.state