src/HOL/Tools/inductive_codegen.ML

--- a/src/HOL/Tools/inductive_codegen.ML	Mon Oct 25 20:24:13 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Oct 25 21:06:56 2010 +0200
@@ -844,7 +844,7 @@
     val test_fn' = !test_fn;
     val dummy_report = ([], false)
     fun test k = (deepen bound (fn i =>
-      (priority ("Search depth: " ^ string_of_int i);
+      (Output.urgent_message ("Search depth: " ^ string_of_int i);
        test_fn' (i, values, k+offset))) start, dummy_report);
   in test end;