# HG changeset patch
# User paulson
# Date 837090162 -7200
# Node ID 58ab3b74a34495c60d1effc76dfa58a1c3eb2cf7
# Parent  763f08fb194fea7b09d1d943198dee767e0b200b
Modified to reject certain inputs -- illustrates error handling

diff -r 763f08fb194f -r 58ab3b74a344 src/FOL/ex/IffOracle.ML
--- 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";  
diff -r 763f08fb194f -r 58ab3b74a344 src/FOL/ex/declIffOracle.ML
--- 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;