# HG changeset patch
# User wenzelm
# Date 1475829994 -7200
# Node ID 0b22328a353cdd5c5a7104d125d31a8675ddeecb
# Parent  cffd5f5372062d5b4afb8eed1f821f1d2ec25db5
more official legacy status;

diff -r cffd5f537206 -r 0b22328a353c src/HOL/Library/Old_SMT.thy
--- a/src/HOL/Library/Old_SMT.thy	Fri Oct 07 10:31:34 2016 +0200
+++ b/src/HOL/Library/Old_SMT.thy	Fri Oct 07 10:46:34 2016 +0200
@@ -142,7 +142,8 @@
 method_setup old_smt = \<open>
   Scan.optional Attrib.thms [] >>
     (fn thms => fn ctxt =>
-      METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts))))
+      (legacy_feature "Proof method \"old_smt\" will be discontinued soon -- use \"smt\" instead";
+       METHOD (fn facts => HEADGOAL (Old_SMT_Solver.smt_tac ctxt (thms @ facts)))))
 \<close> "apply an SMT solver to the current goal"