--- a/CookBook/Recipes/ExternalSolver.thy	Sat Feb 14 13:20:21 2009 +0000
+++ b/CookBook/Recipes/ExternalSolver.thy	Sat Feb 14 16:09:04 2009 +0000
@@ -4,7 +4,7 @@
 begin
 
 
-section {* Executing an External Application *}
+section {* Executing an External Application \label{rec:external}*}
 
 text {*
   {\bf Problem:}
@@ -57,9 +57,11 @@
 
 
 
-section {* Writing an Oracle\label{rec:external} *} 
+section {* Writing an Oracle\label{rec:oracle} *} 
 
 text {*
+  (FIXME: should go into a separate file)
+
   {\bf Problem:}
   You want to use a fast, new decision procedure not based one Isabelle's
   tactics, and you do not care whether it is sound.