src/FOL/ex/IffOracle.thy

--- a/src/FOL/ex/IffOracle.thy	Fri Jan 13 17:39:41 2006 +0100
+++ b/src/FOL/ex/IffOracle.thy	Sat Jan 14 17:14:06 2006 +0100
@@ -40,12 +40,12 @@
 text {* These oracle calls had better fail *}
 
 ML {*
-  (iff_oracle (the_context ()) 5; raise ERROR)
+  (iff_oracle (the_context ()) 5; error "?")
     handle Fail _ => warning "Oracle failed, as expected"
 *}
 
 ML {*
-  (iff_oracle (the_context ()) 1; raise ERROR)
+  (iff_oracle (the_context ()) 1; error "?")
     handle Fail _ => warning "Oracle failed, as expected"
 *}