# HG changeset patch
# User wenzelm
# Date 1003170866 -7200
# Node ID 1aa328cb273a575155d5580f5e447912c2c46291
# Parent  37efbe093d3c20348031a794aa21619dda4e0d78
ring instead of ringS;

diff -r 37efbe093d3c -r 1aa328cb273a src/HOL/Algebra/poly/PolyHomo.thy
--- a/src/HOL/Algebra/poly/PolyHomo.thy	Mon Oct 15 20:34:12 2001 +0200
+++ b/src/HOL/Algebra/poly/PolyHomo.thy	Mon Oct 15 20:34:26 2001 +0200
@@ -12,8 +12,8 @@
   up :: (domain) domain (up_one_not_zero, up_integral)
 
 consts
-  EVAL2	:: ('a::ringS => 'b) => 'b => 'a up => 'b::ringS
-  EVAL	:: 'a::ringS => 'a up => 'a
+  EVAL2	:: "('a::ring => 'b) => 'b => 'a up => 'b::ring"
+  EVAL	:: "'a::ring => 'a up => 'a"
 
 defs
   EVAL2_def	"EVAL2 phi a p ==