# HG changeset patch # User wenzelm # Date 1273668743 -7200 # Node ID 6637878680b039856a68b09942ad19918668dc00 # Parent 952b2b102a0a39778ccc9c3c957e9c46231c532a do not emit legacy_feature warnings here -- users have no chance to disable them; diff -r 952b2b102a0a -r 6637878680b0 src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Wed May 12 14:17:26 2010 +0200 +++ b/src/Pure/old_goals.ML Wed May 12 14:52:23 2010 +0200 @@ -293,7 +293,6 @@ *) fun prepare_proof atomic rths chorn = let - val _ = legacy_feature "Old goal command"; val thy = Thm.theory_of_cterm chorn; val horn = Thm.term_of chorn; val _ = Term.no_dummy_patterns horn handle TERM (msg, _) => error msg; @@ -514,7 +513,6 @@ (*simple version with minimal amount of checking and postprocessing*) fun simple_prove_goal_cterm G f = let - 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;