changeset 31021 | 53642251a04f |
parent 30510 | 4120fc59dd85 |
child 31242 | ed40b987a474 |
--- a/src/HOL/Library/comm_ring.ML Tue Apr 28 19:15:50 2009 +0200 +++ b/src/HOL/Library/comm_ring.ML Wed Apr 29 14:20:26 2009 +0200 @@ -65,7 +65,7 @@ | reif_polex T vs t = polex_pol T $ reif_pol T vs t; (* reification of the equation *) -val TFree (_, cr_sort) = @{typ "'a :: {comm_ring, recpower}"}; +val cr_sort = @{sort "comm_ring_1"}; fun reif_eq thy (eq as Const("op =", Type("fun", [T, _])) $ lhs $ rhs) = if Sign.of_sort thy (T, cr_sort) then