# HG changeset patch
# User wenzelm
# Date 1004904028 -3600
# Node ID 58a2e6750d231cadc2884df11b4e98b37412e399
# Parent  d38b5388e695f5acc62c887b1085ec6f52314759
simplified Proof.init_state:

diff -r d38b5388e695 -r 58a2e6750d23 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Nov 04 21:00:06 2001 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Nov 04 21:00:28 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 (fn thy => Proof.init_state thy None) Proof.enter_forward;
+val enter_forward_proof = node_case Proof.init_state Proof.enter_forward;
 
 
 (** toplevel transitions **)