--- a/src/Doc/Implementation/Logic.thy Sat Aug 17 17:57:10 2019 +0200
+++ b/src/Doc/Implementation/Logic.thy Sat Aug 17 17:59:55 2019 +0200
@@ -579,7 +579,6 @@
\end{mldecls}
\begin{mldecls}
@{index_ML_type thm} \\
- @{index_ML Thm.peek_status: "thm -> {oracle: bool, unfinished: bool, failed: bool}"} \\
@{index_ML Thm.transfer: "theory -> thm -> thm"} \\
@{index_ML Thm.assume: "cterm -> thm"} \\
@{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
@@ -602,13 +601,6 @@
@{index_ML Thm_Deps.all_oracles: "thm list -> (string * term option) list"} \\
\end{mldecls}
- \<^descr> \<^ML>\<open>Thm.peek_status\<close>~\<open>thm\<close> informs about the current status of the
- derivation object behind the given theorem. This is a snapshot of a
- potentially ongoing (parallel) evaluation of proofs. The three Boolean
- values indicate the following: \<^verbatim>\<open>oracle\<close> if the finished part contains some
- oracle invocation; \<^verbatim>\<open>unfinished\<close> if some future proofs are still pending;
- \<^verbatim>\<open>failed\<close> if some future proof has failed, rendering the theorem invalid!
-
\<^descr> \<^ML>\<open>Logic.all\<close>~\<open>a B\<close> produces a Pure quantification \<open>\<And>a. B\<close>, where
occurrences of the atomic term \<open>a\<close> in the body proposition \<open>B\<close> are replaced
by bound variables. (See also \<^ML>\<open>lambda\<close> on terms.)
--- a/src/Pure/proofterm.ML Sat Aug 17 17:57:10 2019 +0200
+++ b/src/Pure/proofterm.ML Sat Aug 17 17:59:55 2019 +0200
@@ -56,7 +56,6 @@
({serial: proof_serial, name: string, prop: term, body: proof_body} -> 'a -> 'a) ->
proof_body list -> 'a -> 'a
val consolidate: proof_body list -> unit
- val peek_status: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
val oracle_ord: oracle * oracle -> order
val thm_ord: pthm * pthm -> order
@@ -290,29 +289,6 @@
in (f {serial = i, name = name, prop = prop, body = body} x', seen') end);
in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
-fun peek_status bodies =
- let
- fun status (PBody {oracles, thms, ...}) x =
- let
- val ((oracle, unfinished, failed), seen) =
- (thms, x) |-> fold (fn (i, thm_node) => fn (st, seen) =>
- if Inttab.defined seen i then (st, seen)
- else
- let val seen' = Inttab.update (i, ()) seen in
- (case Future.peek (thm_node_body thm_node) of
- SOME (Exn.Res body') => status body' (st, seen')
- | SOME (Exn.Exn _) =>
- let val (oracle, unfinished, _) = st
- in ((oracle, unfinished, true), seen') end
- | NONE =>
- let val (oracle, _, failed) = st
- in ((oracle, true, failed), seen') end)
- end);
- in ((oracle orelse not (null oracles), unfinished, failed), seen) end;
- val (oracle, unfinished, failed) =
- #1 (fold status bodies ((false, false, false), Inttab.empty));
- in {oracle = oracle, unfinished = unfinished, failed = failed} end;
-
(* proof body *)
--- a/src/Pure/thm.ML Sat Aug 17 17:57:10 2019 +0200
+++ b/src/Pure/thm.ML Sat Aug 17 17:59:55 2019 +0200
@@ -102,7 +102,6 @@
val proof_body_of: thm -> proof_body
val proof_of: thm -> proof
val consolidate: thm list -> unit
- val peek_status: thm -> {oracle: bool, unfinished: bool, failed: bool}
val future: thm future -> cterm -> thm
val derivation_closed: thm -> bool
val derivation_name: thm -> string
@@ -755,21 +754,6 @@
val consolidate = ignore o proof_bodies_of;
-(* derivation status *)
-
-fun peek_status (Thm (Deriv {promises, body}, _)) =
- let
- val ps = map (Future.peek o snd) promises;
- val bodies = body ::
- map_filter (fn SOME (Exn.Res th) => SOME (raw_body_of th) | _ => NONE) ps;
- val {oracle, unfinished, failed} = Proofterm.peek_status bodies;
- in
- {oracle = oracle,
- unfinished = unfinished orelse exists is_none ps,
- failed = failed orelse exists (fn SOME (Exn.Exn _) => true | _ => false) ps}
- end;
-
-
(* future rule *)
fun future_result i orig_cert orig_shyps orig_prop thm =