315 val sorts = Sorts.union sorts1 sorts2; |
315 val sorts = Sorts.union sorts1 sorts2; |
316 fun mk_cTinst ((a, i), (S, T)) = |
316 fun mk_cTinst ((a, i), (S, T)) = |
317 (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, |
317 (Ctyp {T = TVar ((a, i), S), thy_ref = Theory.check_thy thy, maxidx = i, sorts = sorts}, |
318 Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}); |
318 Ctyp {T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}); |
319 fun mk_ctinst ((x, i), (T, t)) = |
319 fun mk_ctinst ((x, i), (T, t)) = |
320 let val T = Envir.typ_subst_TVars Tinsts T in |
320 let val T = Envir.subst_type Tinsts T in |
321 (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy, |
321 (Cterm {t = Var ((x, i), T), T = T, thy_ref = Theory.check_thy thy, |
322 maxidx = i, sorts = sorts}, |
322 maxidx = i, sorts = sorts}, |
323 Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}) |
323 Cterm {t = t, T = T, thy_ref = Theory.check_thy thy, maxidx = maxidx2, sorts = sorts}) |
324 end; |
324 end; |
325 in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; |
325 in (Vartab.fold (cons o mk_cTinst) Tinsts [], Vartab.fold (cons o mk_ctinst) tinsts []) end; |
1465 |
1465 |
1466 (*Faster normalization: skip assumptions that were lifted over*) |
1466 (*Faster normalization: skip assumptions that were lifted over*) |
1467 fun norm_term_skip env 0 t = Envir.norm_term env t |
1467 fun norm_term_skip env 0 t = Envir.norm_term env t |
1468 | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) = |
1468 | norm_term_skip env n (Const ("all", _) $ Abs (a, T, t)) = |
1469 let |
1469 let |
1470 val T' = Envir.typ_subst_TVars (Envir.type_env env) T |
1470 val T' = Envir.subst_type (Envir.type_env env) T |
1471 (*Must instantiate types of parameters because they are flattened; |
1471 (*Must instantiate types of parameters because they are flattened; |
1472 this could be a NEW parameter*) |
1472 this could be a NEW parameter*) |
1473 in Term.all T' $ Abs (a, T', norm_term_skip env n t) end |
1473 in Term.all T' $ Abs (a, T', norm_term_skip env n t) end |
1474 | norm_term_skip env n (Const ("==>", _) $ A $ B) = |
1474 | norm_term_skip env n (Const ("==>", _) $ A $ B) = |
1475 Logic.mk_implies (A, norm_term_skip env (n - 1) B) |
1475 Logic.mk_implies (A, norm_term_skip env (n - 1) B) |