equal
deleted
inserted
replaced
63 | reif_polex T vs t = polex_pol T $ reif_pol T vs t; |
63 | reif_polex T vs t = polex_pol T $ reif_pol T vs t; |
64 |
64 |
65 (* reification of the equation *) |
65 (* reification of the equation *) |
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 "op ="}, 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 = OldTerm.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); |