author | wenzelm |
Fri, 06 Apr 2012 13:10:45 +0200 | |
changeset 47383 | 003189cebf12 |
parent 47382 | 5b902eeb2a29 |
child 47385 | ee89d066579d |
--- 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