src/Pure/old_goals.ML

   "atomic" indicates if the goal should be wrapped up in the function
   "Goal::prop=>prop" to avoid assumptions being returned separately.
 *)
 fun prepare_proof atomic rths chorn =
   let
-      val _ = warning "Obsolete goal command encountered";
+      val _ = legacy_feature "old goal command";
       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;
       val atoms = atomic andalso
             forall (fn t => not (can Logic.dest_implies t orelse Logic.is_all t)) As;

 val Goal = Goalw [];
 
 (*simple version with minimal amount of checking and postprocessing*)
 fun simple_prove_goal_cterm G f =
   let
-    val _ = warning "Obsolete goal command encountered";
+    val _ = legacy_feature "old goal command";
     val As = Drule.strip_imp_prems G;
     val B = Drule.strip_imp_concl G;
     val asms = map Assumption.assume As;
     fun check NONE = error "prove_goal: tactic failed"
       | check (SOME (thm, _)) = (case nprems_of thm of