| changeset 17984 | bdac047db2a5 |
| parent 17965 | fa380d7d4931 |
| child 17987 | f8b45ab11400 |
--- 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";