--- a/src/Pure/thm.ML Thu Dec 15 22:22:45 2016 +0100
+++ b/src/Pure/thm.ML Fri Dec 16 14:06:31 2016 +0100
@@ -1309,9 +1309,9 @@
val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees);
val ps = map (apsnd (Future.map fulfill_body)) promises;
- val (pthm as (_, (_, prop', _)), proof) =
- Proofterm.unconstrain_thm_proof thy shyps prop ps body;
+ val (pthm, proof) = Proofterm.unconstrain_thm_proof thy shyps prop ps body;
val der' = make_deriv [] [] [pthm] proof;
+ val prop' = Proofterm.thm_node_prop (#2 pthm);
in
Thm (der',
{cert = cert,