diff -r 3e9ae9032273 -r b8cdd3d73022 src/HOL/Tools/Function/scnp_solve.ML
--- a/src/HOL/Tools/Function/scnp_solve.ML	Fri Oct 23 15:33:19 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML	Fri Oct 23 16:22:10 2009 +0200
@@ -73,7 +73,7 @@
 (* SAT solving *)
 val solver = Unsynchronized.ref "auto";
 fun sat_solver x =
-  FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
+  Function_Common.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x
 
 (* "Virtual constructors" for various propositional variables *)
 fun var_constrs (gp as GP (arities, gl)) =