--- a/ProgTutorial/Recipes/Sat.thy	Sun Dec 15 23:49:05 2013 +0000
+++ b/ProgTutorial/Recipes/Sat.thy	Thu Mar 13 17:16:49 2014 +0000
@@ -97,15 +97,15 @@
   @{text [quotes] "dpll"}.
 
   There are also two tactics that make use of SAT solvers. One 
-  is the tactic @{ML sat_tac in sat}. For example 
+  is the tactic @{ML sat_tac in SAT}. For example 
 *}
 
 lemma "True"
-apply(tactic {* sat.sat_tac @{context} 1 *})
+apply(tactic {* SAT.sat_tac @{context} 1 *})
 done
 
 text {*
-  However, for proving anything more exciting using @{ML "sat_tac" in sat} you 
+  However, for proving anything more exciting using @{ML "sat_tac" in SAT} you 
   have to use a SAT solver that can produce a proof. The internal 
   one is not usuable for this. 
 
@@ -113,7 +113,7 @@
   The interface for the external SAT solvers is implemented
   in @{ML_file "HOL/Tools/sat_solver.ML"}. This file contains also a simple
   SAT solver based on the DPLL algorithm. The tactics for SAT solvers are
-  implemented in @{ML_file "HOL/Tools/sat_funcs.ML"}. Functions concerning
+  implemented in @{ML_file "HOL/Tools/sat.ML"}. Functions concerning
   propositional formulas are implemented in @{ML_file
   "HOL/Tools/prop_logic.ML"}. The tables used in the translation function are
   implemented in @{ML_file "Pure/General/table.ML"}.