author | wenzelm |
Wed, 31 Oct 2001 22:02:33 +0100 | |
changeset 12009 | cbd35a736954 |
parent 12008 | 078637472921 |
child 12010 | e1d4df962ac9 |
--- 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 **)