# HG changeset patch
# User wenzelm
# Date 1154610189 -7200
# Node ID c80539928948ca685209100219a98833b726a3c9
# Parent  b7c0bf788f508da822fb976945284f773a418c9e
removed OldGoals.legacy flag (always warn);

diff -r b7c0bf788f50 -r c80539928948 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Thu Aug 03 15:03:08 2006 +0200
+++ b/src/Pure/old_goals.ML	Thu Aug 03 15:03:09 2006 +0200
@@ -48,7 +48,6 @@
 signature OLD_GOALS =
 sig
   include GOALS
-  val legacy: bool ref
   type proof
   val chop: unit -> unit
   val reset_goals: unit -> unit
@@ -90,10 +89,6 @@
 structure OldGoals: OLD_GOALS =
 struct
 
-val legacy = ref false;
-fun warn_obsolete () = if ! legacy then () else warning "Obsolete goal command encountered";
-
-
 (*** Goal package ***)
 
 (*Each level of goal stack includes a proof state and alternative states,
@@ -156,7 +151,7 @@
 *)
 fun prepare_proof atomic rths chorn =
   let
-      val _ = warn_obsolete ();
+      val _ = warning "Obsolete goal command encountered";
       val {thy, t=horn,...} = rep_cterm chorn;
       val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg;
       val (As, B) = Logic.strip_horn horn;
@@ -377,7 +372,7 @@
 (*simple version with minimal amount of checking and postprocessing*)
 fun simple_prove_goal_cterm G f =
   let
-    val _ = warn_obsolete ();
+    val _ = warning "Obsolete goal command encountered";
     val As = Drule.strip_imp_prems G;
     val B = Drule.strip_imp_concl G;
     val asms = map Assumption.assume As;