1220 {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx, |
1220 {thy_ref = Theory.check_thy thy, tags = tags, maxidx = maxidx, |
1221 shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) |
1221 shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) |
1222 end; |
1222 end; |
1223 |
1223 |
1224 (*Internalize sort constraints of type variables*) |
1224 (*Internalize sort constraints of type variables*) |
1225 fun unconstrainT (thm as Thm (_, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = |
1225 fun unconstrainT (thm as Thm (der, args)) = |
1226 let |
1226 let |
|
1227 val Deriv {promises, body} = der; |
|
1228 val {thy_ref, shyps, hyps, tpairs, prop, ...} = args; |
|
1229 |
1227 fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); |
1230 fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); |
1228 |
|
1229 val _ = null hyps orelse err "illegal hyps"; |
1231 val _ = null hyps orelse err "illegal hyps"; |
1230 val _ = null tpairs orelse err "unsolved flex-flex constraints"; |
1232 val _ = null tpairs orelse err "unsolved flex-flex constraints"; |
1231 val tfrees = rev (Term.add_tfree_names prop []); |
1233 val tfrees = rev (Term.add_tfree_names prop []); |
1232 val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); |
1234 val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); |
1233 |
1235 |
1234 val (_, prop') = Logic.unconstrainT shyps prop; |
1236 val ps = map (apsnd (Future.map proof_body_of)) promises; |
1235 in |
1237 val thy = Theory.deref thy_ref; |
1236 Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])), |
1238 val (pthm as (_, (_, prop', _)), proof) = Pt.unconstrain_thm_proof thy shyps prop ps body; |
|
1239 val der' = make_deriv [] [] [pthm] proof; |
|
1240 val _ = Theory.check_thy thy; |
|
1241 in |
|
1242 Thm (der', |
1237 {thy_ref = thy_ref, |
1243 {thy_ref = thy_ref, |
1238 tags = [], |
1244 tags = [], |
1239 maxidx = maxidx_of_term prop', |
1245 maxidx = maxidx_of_term prop', |
1240 shyps = [[]], (*potentially redundant*) |
1246 shyps = [[]], (*potentially redundant*) |
1241 hyps = hyps, |
1247 hyps = [], |
1242 tpairs = tpairs, |
1248 tpairs = [], |
1243 prop = prop'}) |
1249 prop = prop'}) |
1244 end; |
1250 end; |
1245 |
1251 |
1246 fun legacy_unconstrainT |
1252 fun legacy_unconstrainT |
1247 (Ctyp {thy_ref = thy_ref1, T, ...}) |
1253 (Ctyp {thy_ref = thy_ref1, T, ...}) |