--- 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;