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