changeset 47383 | 003189cebf12 |
parent 47348 | 9a82999ebbd6 |
child 47576 | b32aae03e3d6 |
--- a/src/Tools/quickcheck.ML Fri Apr 06 12:45:56 2012 +0200 +++ b/src/Tools/quickcheck.ML Fri Apr 06 13:10:45 2012 +0200 @@ -343,7 +343,7 @@ val cs = space_explode " " s in if forall (fn c => c = "expand" orelse c = "interpret") cs then cs - else (Output.warning ("Invalid quickcheck_locale setting: falling back to the default setting."); + else (warning ("Invalid quickcheck_locale setting: falling back to the default setting."); ["interpret", "expand"]) end