src/Pure/thm.ML

       val thy = theory_of_thm thm;
 
       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) =
         Proofterm.thm_proof thy (classrel_proof thy) (arity_proof thy)
           name_pos shyps hyps prop ps body;
       val der' = make_deriv [] [] [pthm] proof;
     in Thm (der', args) end);
 
 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;