# HG changeset patch
# User wenzelm
# Date 1129936930 -7200
# Node ID bdac047db2a5592d2a4f9bf19cdd7792bbdb5fe6
# Parent  89103008502f719d6787c329aa0924e6e7ec6dee
legacy = ref true for the time being -- avoid volumious warnings;

diff -r 89103008502f -r bdac047db2a5 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";