equal
deleted
inserted
replaced
66 val cr_sort = @{sort "comm_ring_1"}; |
66 val cr_sort = @{sort "comm_ring_1"}; |
67 |
67 |
68 fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) = |
68 fun reif_eq thy (eq as Const(@{const_name HOL.eq}, Type("fun", [T, _])) $ lhs $ rhs) = |
69 if Sign.of_sort thy (T, cr_sort) then |
69 if Sign.of_sort thy (T, cr_sort) then |
70 let |
70 let |
71 val fs = OldTerm.term_frees eq; |
71 val fs = Misc_Legacy.term_frees eq; |
72 val cvs = cterm_of thy (HOLogic.mk_list T fs); |
72 val cvs = cterm_of thy (HOLogic.mk_list T fs); |
73 val clhs = cterm_of thy (reif_polex T fs lhs); |
73 val clhs = cterm_of thy (reif_polex T fs lhs); |
74 val crhs = cterm_of thy (reif_polex T fs rhs); |
74 val crhs = cterm_of thy (reif_polex T fs rhs); |
75 val ca = ctyp_of thy T; |
75 val ca = ctyp_of thy T; |
76 in (ca, cvs, clhs, crhs) end |
76 in (ca, cvs, clhs, crhs) end |