equal
deleted
inserted
replaced
1543 |
1543 |
1544 (*Faster normalization: skip assumptions that were lifted over*) |
1544 (*Faster normalization: skip assumptions that were lifted over*) |
1545 fun norm_term_skip env 0 t = Envir.norm_term env t |
1545 fun norm_term_skip env 0 t = Envir.norm_term env t |
1546 | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) = |
1546 | norm_term_skip env n (Const ("Pure.all", _) $ Abs (a, T, t)) = |
1547 let |
1547 let |
1548 val T' = Envir.subst_type (Envir.type_env env) T |
1548 val T' = Envir.norm_type (Envir.type_env env) T |
1549 (*Must instantiate types of parameters because they are flattened; |
1549 (*Must instantiate types of parameters because they are flattened; |
1550 this could be a NEW parameter*) |
1550 this could be a NEW parameter*) |
1551 in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end |
1551 in Logic.all_const T' $ Abs (a, T', norm_term_skip env n t) end |
1552 | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) = |
1552 | norm_term_skip env n (Const ("Pure.imp", _) $ A $ B) = |
1553 Logic.mk_implies (A, norm_term_skip env (n - 1) B) |
1553 Logic.mk_implies (A, norm_term_skip env (n - 1) B) |