Modified to reject certain inputs -- illustrates error handling

--- a/src/FOL/ex/IffOracle.ML	Thu Jul 11 15:00:38 1996 +0200
+++ b/src/FOL/ex/IffOracle.ML	Thu Jul 11 15:02:42 1996 +0200
@@ -6,8 +6,14 @@
 Example of how to use an oracle
 *)
 
-invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 0);
-invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5);
+invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 2);
 invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 10);
 #der(rep_thm it);
 
+(*These oracle calls had better fail*)
+
+(invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 5); 
+ raise ERROR) handle IffOracleExn _ => writeln"Failed, as expected";  
+
+(invoke_oracle (IffOracle.thy, sign_of IffOracle.thy, IffOracleExn 0); 
+ raise ERROR) handle IffOracleExn _ => writeln"Failed, as expected";  

--- a/src/FOL/ex/declIffOracle.ML	Thu Jul 11 15:00:38 1996 +0200
+++ b/src/FOL/ex/declIffOracle.ML	Thu Jul 11 15:02:42 1996 +0200
@@ -15,10 +15,13 @@
 
 val iff = Const("op <->", [oT,oT]--->oT);
 
-fun mk_iff 0 = Const("True", oT)
+fun mk_iff 1 = Free("P", oT)
   | mk_iff n = iff $ Free("P", oT) $ mk_iff (n-1);
 
 val Trueprop = Const("Trueprop",oT-->propT);
 
-(*Oracle makes tautologies of the form "P <-> P <-> P <-> P <-> True"*)
-fun mk_iff_oracle (sign, IffOracleExn n) = Trueprop $ mk_iff (2*n);
+(*Oracle makes tautologies of the form "P <-> P <-> P <-> P"*)
+fun mk_iff_oracle (sign, IffOracleExn n) = 
+    if n>0 andalso n mod 2 = 0 
+    then Trueprop $ mk_iff n
+    else raise IffOracleExn n;