src/Pure/Isar/calculation.ML
changeset 58011 bc6bced136e5
parent 56894 fa12200276bf
child 58028 e4250d370657
--- a/src/Pure/Isar/calculation.ML	Tue Aug 19 18:21:29 2014 +0200
+++ b/src/Pure/Isar/calculation.ML	Tue Aug 19 23:17:51 2014 +0200
@@ -14,10 +14,10 @@
   val sym_del: attribute
   val symmetric: attribute
   val also: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
-  val also_cmd: (Facts.ref * Attrib.src list) list option ->
+  val also_cmd: (Facts.ref * Token.src list) list option ->
     bool -> Proof.state -> Proof.state Seq.result Seq.seq
   val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.result Seq.seq
-  val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool ->
+  val finally_cmd: (Facts.ref * Token.src list) list option -> bool ->
     Proof.state -> Proof.state Seq.result Seq.seq
   val moreover: bool -> Proof.state -> Proof.state
   val ultimately: bool -> Proof.state -> Proof.state