equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 ML {* |
5 ML {* |
6 fun const_rsp qtys lthy const = |
6 fun const_rsp qtys lthy const = |
7 let |
7 let |
8 val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy) |
8 val nty = Quotient_Term.derive_qtyp qtys (fastype_of const) lthy |
9 val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); |
9 val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty); |
10 in |
10 in |
11 HOLogic.mk_Trueprop (rel $ const $ const) |
11 HOLogic.mk_Trueprop (rel $ const $ const) |
12 end |
12 end |
13 *} |
13 *} |