src/HOL/ex/Iff_Oracle.thy
changeset 50126 3dec88149176
parent 42814 5af15f1e2ef6
child 58889 5b7a9633cfa8
     1.1 --- a/src/HOL/ex/Iff_Oracle.thy	Mon Nov 19 18:01:48 2012 +0100
     1.2 +++ b/src/HOL/ex/Iff_Oracle.thy	Mon Nov 19 20:23:47 2012 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4  
     1.5  ML {* iff_oracle (@{theory}, 2) *}
     1.6  ML {* iff_oracle (@{theory}, 10) *}
     1.7 -ML {* Thm.status_of (iff_oracle (@{theory}, 10)) *}
     1.8 +ML {* Thm.peek_status (iff_oracle (@{theory}, 10)) *}
     1.9  
    1.10  text {* These oracle calls had better fail. *}
    1.11