# HG changeset patch
# User kleing
# Date 1081835107 -7200
# Node ID e1a196985fc8b68d647499c18b3880e64591a1ae
# Parent  e0c0179100c9c9875961c25ec13952a3a32c28bb
export thisN

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 =