# HG changeset patch
# User wenzelm
# Date 950037249 -3600
# Node ID ca3997312f47bd3ccf13d449f66368a05c6243c3
# Parent  4816ba139574bac3a9c399b02774544208538392
added forget_proof;

diff -r 4816ba139574 -r ca3997312f47 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Feb 08 20:13:58 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 08 20:14:09 2000 +0100
@@ -378,6 +378,11 @@
   OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
     (P.marg_comment >> IsarThy.skip_proof);
 
+val forget_proofP =
+  OuterSyntax.improper_command "oops" "forget proof" K.qed_global
+    (P.marg_comment >> IsarThy.forget_proof);
+
+
 
 (* proof steps *)
 
@@ -624,9 +629,9 @@
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   defP, fixP, letP, thenP, thenceP, fromP, withP, noteP, beginP, endP,
   nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
-  skip_proofP, deferP, preferP, applyP, then_applyP, proofP, alsoP,
-  finallyP, backP, cannot_undoP, clear_undosP, redoP, undos_proofP,
-  kill_proofP, undoP,
+  skip_proofP, forget_proofP, deferP, preferP, applyP, then_applyP,
+  proofP, alsoP, finallyP, backP, cannot_undoP, clear_undosP, redoP,
+  undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
   pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
   print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,
diff -r 4816ba139574 -r ca3997312f47 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Tue Feb 08 20:13:58 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Tue Feb 08 20:14:09 2000 +0100
@@ -122,7 +122,6 @@
   val then_tac: Method.text -> ProofHistory.T -> ProofHistory.T
   val proof: (Comment.interest * (Method.text * Comment.interest) option) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
-  val kill_proof: ProofHistory.T -> theory
   val qed: (Method.text * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
   val terminal_proof: ((Method.text * Comment.interest) * (Method.text * Comment.interest) option)
@@ -130,6 +129,7 @@
   val immediate_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val default_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val skip_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
+  val forget_proof: Comment.text -> Toplevel.transition -> Toplevel.transition
   val get_thmss: (string * Args.src list) list -> Proof.state -> thm list
   val also: ((string * Args.src list) list * Comment.interest) option * Comment.text
     -> Toplevel.transition -> Toplevel.transition
@@ -402,8 +402,6 @@
 
 (* global endings *)
 
-val kill_proof = Proof.theory_of o ProofHistory.current;
-
 fun global_result finish = Toplevel.proof_to_theory (fn prf =>
   let
     val state = ProofHistory.current prf;
@@ -426,6 +424,8 @@
 fun default_proof comment = local_default_proof o global_default_proof;
 fun skip_proof comment = local_skip_proof o global_skip_proof;
 
+fun forget_proof comment = Toplevel.proof_to_theory (Proof.theory_of o ProofHistory.current);
+
 
 (* calculational proof commands *)