# HG changeset patch
# User wenzelm
# Date 1212097605 -7200
# Node ID f8255a5dc3a8ee14f08901197a7b31d5ccf6ee0f
# Parent  4593b9f4ba429ec326197e60072c82a7ad085822
legacy_feature: no proof context in simpset;

diff -r 4593b9f4ba42 -r f8255a5dc3a8 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Thu May 29 23:46:43 2008 +0200
+++ b/src/Pure/meta_simplifier.ML	Thu May 29 23:46:45 2008 +0200
@@ -381,7 +381,8 @@
 fun activate_context thy (ss as Simpset ({context = SOME ctxt, ...}, _)) =
       context (Context.transfer_proof (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt) ss
   | activate_context thy ss =
-     (warning "Simplifier: no proof context in simpset -- fallback to theory context!";
+     (legacy_feature ("Simplifier: no proof context in simpset -- fallback to theory context!" ^
+       Position.str_of (Position.thread_data ()));
       theory_context thy ss);