# HG changeset patch
# User wenzelm
# Date 1004562153 -3600
# Node ID cbd35a736954d9f4f6ea3c4e9fb3201b168d1a1f
# Parent  078637472921715805f9f1b49aeaa0dd85549394
Proof.init_state thy None;

diff -r 078637472921 -r cbd35a736954 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Oct 31 22:02:11 2001 +0100
+++ b/src/Pure/Isar/toplevel.ML	Wed Oct 31 22:02:33 2001 +0100
@@ -155,7 +155,7 @@
 val sign_of = Theory.sign_of o theory_of;
 val proof_of = node_case (fn _ => raise UNDEF) I;
 
-val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;
+val enter_forward_proof = node_case (fn thy => Proof.init_state thy None) Proof.enter_forward;
 
 
 (** toplevel transitions **)