legacy = ref true for the time being -- avoid volumious warnings;
authorwenzelm
Sat, 22 Oct 2005 01:22:10 +0200
changeset 17984 bdac047db2a5
parent 17983 89103008502f
child 17985 d5d576b72371
legacy = ref true for the time being -- avoid volumious warnings;
src/Pure/goals.ML
--- a/src/Pure/goals.ML	Fri Oct 21 18:20:29 2005 +0200
+++ b/src/Pure/goals.ML	Sat Oct 22 01:22:10 2005 +0200
@@ -91,7 +91,7 @@
 structure OldGoals: OLD_GOALS =
 struct
 
-val legacy = ref false;
+val legacy = ref true;
 fun warn_obsolete () = if ! legacy then () else warning "Obsolete goal command encountered";