| changeset 27312 | 2a884461a9f3 |
| parent 27022 | f8255a5dc3a8 |
| child 27558 | 33f215fa079e |
| 27311:aa28b1d33866 | 27312:2a884461a9f3 |
|---|---|
376 fun context ctxt = |
376 fun context ctxt = |
377 map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt)); |
377 map_simpset1 (fn (rules, prems, bounds, depth, _) => (rules, prems, bounds, depth, SOME ctxt)); |
378 |
378 |
379 val theory_context = context o ProofContext.init; |
379 val theory_context = context o ProofContext.init; |
380 |
380 |
381 fun activate_context thy (ss as Simpset ({context = SOME ctxt, ...}, _)) = |
381 fun activate_context thy ss = |
382 context (Context.transfer_proof (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt) ss |
382 let |
383 | activate_context thy ss = |
383 val ctxt = the_context ss; |
384 (legacy_feature ("Simplifier: no proof context in simpset -- fallback to theory context!" ^ |
384 val ctxt' = Context.transfer_proof (Theory.merge (thy, ProofContext.theory_of ctxt)) ctxt; |
385 Position.str_of (Position.thread_data ())); |
385 in context ctxt' ss end; |
386 theory_context thy ss); |
|
387 |
386 |
388 |
387 |
389 (* maintain simp rules *) |
388 (* maintain simp rules *) |
390 |
389 |
391 (* FIXME: it seems that the conditions on extra variables are too liberal if |
390 (* FIXME: it seems that the conditions on extra variables are too liberal if |