# 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));