--- 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 *)