# HG changeset patch
# User webertj
# Date 1166201467 -3600
# Node ID 2cfc838297ff8b848978bf3d5fe242becc0f627f
# Parent  13e9febe308014dd9bfca0e69bb6d3f5fc9da61a
tracing instead of warning

diff -r 13e9febe3080 -r 2cfc838297ff src/FOL/ex/IffOracle.thy
--- a/src/FOL/ex/IffOracle.thy	Fri Dec 15 00:08:50 2006 +0100
+++ b/src/FOL/ex/IffOracle.thy	Fri Dec 15 17:51:07 2006 +0100
@@ -37,16 +37,16 @@
 ML {* iff_oracle (the_context ()) 10 *}
 ML {* #der (Thm.rep_thm it) *}
 
-text {* These oracle calls had better fail *}
+text {* These oracle calls had better fail. *}
 
 ML {*
   (iff_oracle (the_context ()) 5; error "?")
-    handle Fail _ => warning "Oracle failed, as expected"
+    handle Fail _ => tracing "Oracle failed, as expected"
 *}
 
 ML {*
   (iff_oracle (the_context ()) 1; error "?")
-    handle Fail _ => warning "Oracle failed, as expected"
+    handle Fail _ => tracing "Oracle failed, as expected"
 *}