# HG changeset patch
# User wenzelm
# Date 1535889235 -7200
# Node ID 7f0151c951e34da6075efc2a40eadd02b4fb16b4
# Parent  cca5ca811714ddf9037704d435cbc89149345185
clarified signature;

diff -r cca5ca811714 -r 7f0151c951e3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Sep 02 13:21:15 2018 +0200
+++ b/src/Pure/Isar/proof.ML	Sun Sep 02 13:53:55 2018 +0200
@@ -33,7 +33,6 @@
   val enter_forward: state -> state
   val enter_chain: state -> state
   val enter_backward: state -> state
-  val has_bottom_goal: state -> bool
   val using_facts: thm list -> state -> state
   val pretty_state: state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.result Seq.seq
@@ -95,6 +94,7 @@
   val end_block: state -> state
   val begin_notepad: context -> state
   val end_notepad: state -> context
+  val is_notepad: state -> bool
   val proof: Method.text_range option -> state -> state Seq.result Seq.seq
   val defer: int -> state -> state
   val prefer: int -> state -> state
@@ -326,17 +326,6 @@
 val before_qed = #before_qed o #2 o current_goal;
 
 
-(* bottom goal *)
-
-fun has_bottom_goal (State stack) =
-  let
-    fun bottom [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
-      | bottom [Node {goal, ...}] = is_some goal
-      | bottom [] = false
-      | bottom (_ :: rest) = bottom rest;
-  in bottom (op :: (Stack.dest stack)) end;
-
-
 (* nested goal *)
 
 fun map_goal f (State stack) =
@@ -904,6 +893,14 @@
   #> close_block
   #> context_of;
 
+fun is_notepad (State stack) =
+  let
+    fun bottom_goal [Node {goal = SOME _, ...}, Node {goal = NONE, ...}] = true
+      | bottom_goal [Node {goal = SOME _, ...}] = true
+      | bottom_goal [] = false
+      | bottom_goal (_ :: rest) = bottom_goal rest;
+  in not (bottom_goal (op :: (Stack.dest stack))) end;
+
 
 (* sub-proofs *)
 
diff -r cca5ca811714 -r 7f0151c951e3 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Sep 02 13:21:15 2018 +0200
+++ b/src/Pure/Isar/toplevel.ML	Sun Sep 02 13:53:55 2018 +0200
@@ -519,7 +519,7 @@
 
 fun forget_proof strict = transaction (fn _ =>
   (fn Proof (prf, (_, orig_gthy)) =>
-        if strict andalso not (Proof.has_bottom_goal (Proof_Node.current prf))
+        if strict andalso 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));