# HG changeset patch
# User wenzelm
# Date 1535890483 -7200
# Node ID cefaac3d24ffce5aba370a55347cfc832b37da9f
# Parent  7f0151c951e34da6075efc2a40eadd02b4fb16b4
no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;

diff -r 7f0151c951e3 -r cefaac3d24ff src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Sep 02 13:53:55 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Sep 02 14:14:43 2018 +0200
@@ -65,7 +65,7 @@
     (local_theory -> Proof.state) -> transition -> transition
   val theory_to_proof: (theory -> Proof.state) -> transition -> transition
   val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition
-  val forget_proof: bool -> transition -> transition
+  val forget_proof: transition -> transition
   val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
   val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition
   val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition
@@ -517,10 +517,10 @@
 
 end;
 
-fun forget_proof strict = transaction (fn _ =>
+val forget_proof = transaction (fn _ =>
   (fn Proof (prf, (_, orig_gthy)) =>
-        if strict andalso Proof.is_notepad (Proof_Node.current prf)
-        then raise UNDEF else Theory (orig_gthy, NONE)
+        if Proof.is_notepad (Proof_Node.current prf) then raise UNDEF
+        else Theory (orig_gthy, NONE)
     | Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE)
     | _ => raise UNDEF));
 
@@ -634,7 +634,7 @@
 
 in
 
-val reset_theory = reset_state is_theory (forget_proof false);
+val reset_theory = reset_state is_theory forget_proof;
 
 val reset_proof =
   reset_state is_proof
diff -r 7f0151c951e3 -r cefaac3d24ff src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Sep 02 13:53:55 2018 +0200
+++ b/src/Pure/Pure.thy	Sun Sep 02 14:14:43 2018 +0200
@@ -916,7 +916,7 @@
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>oops\<close> "forget proof"
-    (Scan.succeed (Toplevel.forget_proof true));
+    (Scan.succeed Toplevel.forget_proof);
 
 in end\<close>