diff -r e0c0179100c9 -r e1a196985fc8 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 13 07:25:46 2004 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Apr 13 07:45:07 2004 +0200
@@ -122,6 +122,7 @@
   val begin_block: state -> state
   val end_block: state -> state Seq.seq
   val next_block: state -> state
+  val thisN: string
 end;
 
 structure Proof: PROOF =