activate_context: strict the_context, no fallback on theory context;

--- 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 *)