# HG changeset patch
# User wenzelm
# Date 1214057929 -7200
# Node ID 2a884461a9f37f96fb3756c8f98ada6d4bf055d4
# Parent  aa28b1d33866b7565a7aec9ec1380f4b463c134b
activate_context: strict the_context, no fallback on theory context;

diff -r aa28b1d33866 -r 2a884461a9f3 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Fri Jun 20 23:37:24 2008 +0200
+++ b/src/Pure/meta_simplifier.ML	Sat Jun 21 16:18:49 2008 +0200
@@ -378,12 +378,11 @@
 
 val theory_context = context o ProofContext.init;
 
-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 =
-     (legacy_feature ("Simplifier: no proof context in simpset -- fallback to theory context!" ^
-       Position.str_of (Position.thread_data ()));
-      theory_context thy ss);
+fun activate_context thy ss =
+  let
+    val ctxt = the_context ss;
+    val ctxt' = Context.transfer_proof (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt;
+  in context ctxt' ss end;
 
 
 (* maintain simp rules *)