author | wenzelm |
Tue, 25 Oct 2005 18:18:58 +0200 | |
changeset 17987 | f8b45ab11400 |
parent 17986 | 0450847646c3 |
child 17988 | 47f81afce1b4 |
src/Pure/goals.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/goals.ML Tue Oct 25 18:18:57 2005 +0200 +++ b/src/Pure/goals.ML Tue Oct 25 18:18:58 2005 +0200 @@ -91,7 +91,7 @@ structure OldGoals: OLD_GOALS = struct -val legacy = ref true; +val legacy = ref false; fun warn_obsolete () = if ! legacy then () else warning "Obsolete goal command encountered";