equal
deleted
inserted
replaced
474 let |
474 let |
475 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
475 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
476 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
476 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
477 in |
477 in |
478 if resrel <> needrel |
478 if resrel <> needrel |
|
479 then term_mismatch "regularize(bex1_res)" ctxt resrel needrel |
|
480 else mk_bexeq $ resrel $ subtrm |
|
481 end |
|
482 |
|
483 | (Const (@{const_name "Bex1"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t, Const (@{const_name "Ex1"}, ty') $ t') => |
|
484 let |
|
485 val subtrm = apply_subt (regularize_trm ctxt) (t, t') |
|
486 val needrel = Syntax.check_term ctxt (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) |
|
487 in |
|
488 if resrel <> needrel |
479 then term_mismatch "regularize(bex1)" ctxt resrel needrel |
489 then term_mismatch "regularize(bex1)" ctxt resrel needrel |
480 else mk_bexeq $ resrel $ subtrm |
490 else mk_bexeq $ resrel $ subtrm |
481 end |
491 end |
482 |
492 |
483 | (* equalities need to be replaced by appropriate equivalence relations *) |
493 | (* equalities need to be replaced by appropriate equivalence relations *) |