src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Tue May 09 11:00:32 2006 +0200
+++ b/src/HOL/HOL.thy	Tue May 09 14:18:40 2006 +0200
@@ -1410,8 +1410,5 @@
   "op =" (* an intermediate solution for polymorphic equality *)
     ml (infixl 6 "=")
     haskell (infixl 4 "==")
-  arbitrary
-    ml ("raise/ (Fail/ \"non-defined-result\")")
-    haskell ("error/ \"non-defined result\"")
 
 end