tuned

--- a/src/HOL/Library/Eval.thy	Fri Mar 07 16:46:57 2008 +0100
+++ b/src/HOL/Library/Eval.thy	Sun Mar 09 07:57:30 2008 +0100
@@ -33,7 +33,6 @@
 subsubsection {* Class @{term term_of} *}
 
 class term_of = rtype +
-  constrains typ_of :: "'a\<Colon>{} itself \<Rightarrow> rtype"
   fixes term_of :: "'a \<Rightarrow> term"
 
 lemma term_of_anything: "term_of x \<equiv> t"