diff -r 4f9803829625 -r 564ea783ace8 src/HOL/Library/Eval_Witness.thy
--- a/src/HOL/Library/Eval_Witness.thy	Wed Jan 21 18:37:44 2009 +0100
+++ b/src/HOL/Library/Eval_Witness.thy	Wed Jan 21 23:40:23 2009 +0100
@@ -32,7 +32,7 @@
   with the oracle.  
 *}
 
-class ml_equiv = type
+class ml_equiv
 
 text {*
   Instances of @{text "ml_equiv"} should only be declared for those types,