--- 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,