author | wenzelm |
Sat, 22 Oct 2005 01:22:10 +0200 | |
changeset 17984 | bdac047db2a5 |
parent 17983 | 89103008502f |
child 17985 | d5d576b72371 |
src/Pure/goals.ML | file | annotate | diff | comparison | revisions |
--- 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";