equal
deleted
inserted
replaced
400 |
400 |
401 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
401 fun regularize_trm_chk ctxt (rtrm, qtrm) = |
402 regularize_trm ctxt (rtrm, qtrm) |
402 regularize_trm ctxt (rtrm, qtrm) |
403 |> Syntax.check_term ctxt |
403 |> Syntax.check_term ctxt |
404 |
404 |
|
405 |
405 (*********************) |
406 (*********************) |
406 (* Rep/Abs Injection *) |
407 (* Rep/Abs Injection *) |
407 (*********************) |
408 (*********************) |
408 |
409 |
409 (* |
410 (* |
428 Otherwise the type of the constant needs lifting, we put |
429 Otherwise the type of the constant needs lifting, we put |
429 and Rep/Abs around it. |
430 and Rep/Abs around it. |
430 |
431 |
431 For free variables: |
432 For free variables: |
432 |
433 |
433 * We put aRep/Abs around it if the type needs lifting. |
434 * We put a Rep/Abs around it if the type needs lifting. |
434 |
435 |
435 Vars case cannot occur. |
436 Vars case cannot occur. |
436 *) |
437 *) |
437 |
438 |
438 fun mk_repabs ctxt (T, T') trm = |
439 fun mk_repabs ctxt (T, T') trm = |