# HG changeset patch
# User wenzelm
# Date 1565630973 -7200
# Node ID 9a9003b5c0c164555cfcf626ee50e1a41f4560b3
# Parent  60005f96d2326c2dd3733cb5f29cf81884018d35
more robust -- notably for metis, which tends to accumulate tpairs;

diff -r 60005f96d232 -r 9a9003b5c0c1 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Mon Aug 12 18:53:02 2019 +0200
+++ b/src/Pure/thm.ML	Mon Aug 12 19:29:33 2019 +0200
@@ -1007,8 +1007,7 @@
       val Deriv {promises, body} = der;
       val {shyps, hyps, prop, tpairs, ...} = args;
 
-      fun err msg = raise THM ("name_derivation: " ^ msg, 0, [thm]);
-      val _ = null tpairs orelse err "bad flex-flex constraints";
+      val _ = null tpairs orelse raise THM ("name_derivation: bad flex-flex constraints", 0, [thm]);
 
       val ps = map (apsnd (Future.map fulfill_body)) promises;
       val (pthm, proof) =
@@ -1019,7 +1018,8 @@
 
 fun close_derivation pos =
   solve_constraints #> (fn thm =>
-    if derivation_closed thm then thm else name_derivation ("", pos) thm);
+    if not (null (tpairs_of thm)) orelse derivation_closed thm then thm
+    else name_derivation ("", pos) thm);
 
 val trim_context = solve_constraints #> trim_context_thm;