author | wenzelm |
Wed, 04 Jan 2006 00:52:43 +0100 | |
changeset 18561 | b0e134637479 |
parent 18560 | 6b4570eb22d2 |
child 18562 | 15178f4aa203 |
--- a/src/Pure/Isar/isar_syn.ML Wed Jan 04 00:52:42 2006 +0100 +++ b/src/Pure/Isar/isar_syn.ML Wed Jan 04 00:52:43 2006 +0100 @@ -513,7 +513,7 @@ val forget_proofP = OuterSyntax.command "oops" "forget proof" (K.tag_proof K.qed_global) - (Scan.succeed IsarThy.forget_proof); + (Scan.succeed Toplevel.forget_proof); (* proof steps *)