--- a/CookBook/Recipes/ExternalSolver.thy	Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/Recipes/ExternalSolver.thy	Sat Feb 07 12:05:02 2009 +0000
@@ -73,8 +73,8 @@
   \begin{readmore}
   A short introduction to oracles can be found in [isar-ref: no suitable label
   for section 3.11]. A simple example, which we will slightly extend here,
-  is given in @{ML_file "FOL/ex/IffOracle"}. The raw interface for adding
-  oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm"}.
+  is given in @{ML_file "FOL/ex/IffOracle.thy"}. The raw interface for adding
+  oracles is @{ML add_oracle in Thm} in @{ML_file "Pure/thm.ML"}.
   \end{readmore}
 
   For our explanation here, we restrict ourselves to decide propositional