# HG changeset patch
# User wenzelm
# Date 1481736138 -3600
# Node ID a504a3dec35a46e7d557bbcdaa6ac8b1453122fb
# Parent  7141a3a4dc835e424e534c0d4d5c1a1133ddeab2
more careful derivation_closed / close_derivation;

diff -r 7141a3a4dc83 -r a504a3dec35a src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Wed Dec 14 16:59:41 2016 +0100
+++ b/src/Pure/more_thm.ML	Wed Dec 14 18:22:18 2016 +0100
@@ -452,8 +452,7 @@
 (* close_derivation *)
 
 fun close_derivation thm =
-  if Thm.derivation_name thm = "" then Thm.name_derivation "" thm
-  else thm;
+  if Thm.derivation_closed thm then thm else Thm.name_derivation "" thm;
 
 
 (* user renaming of parameters in a subgoal *)
diff -r 7141a3a4dc83 -r a504a3dec35a src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed Dec 14 16:59:41 2016 +0100
+++ b/src/Pure/proofterm.ML	Wed Dec 14 18:22:18 2016 +0100
@@ -60,6 +60,8 @@
 
   (** primitive operations **)
   val proofs_enabled: unit -> bool
+  val atomic_proof: proof -> bool
+  val compact_proof: proof -> bool
   val proof_combt: proof * term list -> proof
   val proof_combt': proof * term option list -> proof
   val proof_combP: proof * proof list -> proof
@@ -357,6 +359,19 @@
 
 (***** proof objects with different levels of detail *****)
 
+fun atomic_proof prf =
+  (case prf of
+    Abst _ => false
+  | AbsP _ => false
+  | op % _ => false
+  | op %% _ => false
+  | Promise _ => false
+  | _ => true);
+
+fun compact_proof (prf % _) = compact_proof prf
+  | compact_proof (prf1 %% prf2) = atomic_proof prf2 andalso compact_proof prf1
+  | compact_proof prf = atomic_proof prf;
+
 fun (prf %> t) = prf % SOME t;
 
 val proof_combt = Library.foldl (op %>);
diff -r 7141a3a4dc83 -r a504a3dec35a src/Pure/thm.ML
--- a/src/Pure/thm.ML	Wed Dec 14 16:59:41 2016 +0100
+++ b/src/Pure/thm.ML	Wed Dec 14 18:22:18 2016 +0100
@@ -89,6 +89,7 @@
   val join_proofs: 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
   val name_derivation: string -> thm -> thm
   val axiom: theory -> string -> thm
@@ -655,6 +656,10 @@
 (* closed derivations with official name *)
 
 (*non-deterministic, depends on unknown promises*)
+fun derivation_closed (Thm (Deriv {body, ...}, _)) =
+  Proofterm.compact_proof (Proofterm.proof_of body);
+
+(*non-deterministic, depends on unknown promises*)
 fun derivation_name (Thm (Deriv {body, ...}, {shyps, hyps, prop, ...})) =
   Proofterm.get_name shyps hyps prop (Proofterm.proof_of body);