diff -r b38c5b9cf590 -r a265e41cc33b src/HOL/Tools/Function/scnp_solve.ML
--- a/src/HOL/Tools/Function/scnp_solve.ML	Sun May 04 19:01:36 2014 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML	Sun May 04 19:08:29 2014 +0200
@@ -73,7 +73,7 @@
 (* SAT solving *)
 val solver = Unsynchronized.ref "auto";
 fun sat_solver x =
-  Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
+  Function_Common.PROFILE "sat_solving..." (SAT_Solver.invoke_solver (!solver)) x
 
 (* "Virtual constructors" for various propositional variables *)
 fun var_constrs (gp as GP (arities, _)) =
@@ -250,7 +250,7 @@
   in
     get_first
       (fn l => case sat_solver (encode bits gp l) of
-                 SatSolver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
+                 SAT_Solver.SATISFIABLE f => SOME (mk_certificate bits l gp f)
                | _ => NONE)
       labels
   end