# HG changeset patch
# User haftmann
# Date 1205045850 -3600
# Node ID d64510d3c7b7336f1d68f2476b65bce3c7471d32
# Parent  b7d8c2338585a245f559624acfcd125ae5e6dc0d
tuned

diff -r b7d8c2338585 -r d64510d3c7b7 src/HOL/Library/Eval.thy
--- 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"